Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Canonical terms for the concat function in this blog post: http://spire-lang.org/blog/2014/01/15/modeling-elimination-of-described-types/
λ A m n
ind
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₁
`Arg
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₂
`Arg A (λ _ `Rec n₂ (`End (con (there here , n₂ , refl)))))
, tt)
t₁))
m)
(λ _ `Rec n₁ (`End (con (there here , n₁ , refl)))))
, tt)
t))
(λ n₁ xss
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₂
`Arg A (λ _ `Rec n₂ (`End (con (there here , n₂ , refl)))))
, tt)
t))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ u _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u t,c
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
u c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
((λ q ih
elimEq tt
(λ u₁ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₂ con (here , refl)) u q)
,
(λ n,q ih,tt
elimEq tt
(λ u₁ q
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₂
ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u₁ t,c₁
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u₁)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₂ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
u₁ c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
((λ q ih
elimEq tt
(λ u₂ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₃ n₃) u₁ q)
,
(λ n,q₁ ih,tt₁
elimEq tt
(λ u₂ q
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₃ con (there here , proj₁ ih,tt₁ n₃ , refl)) u₁ (proj₂ n,q₁))
, tt)
(proj₁ t,c₁) (proj₂ t,c₁))
n₂ (proj₁ ih,tt n₂))
u (proj₂ n,q))
, tt)
(proj₁ t,c) (proj₂ t,c))
n₁ m))
(λ n₁ t,c
case
(λ t
(c
: El
(case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₂
`Arg
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t₁))
m)
(λ _ `Rec n₂ (`End (con (there here , n₂ , refl)))))
, tt)
t)
(λ n₂
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₃
`Arg
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₂
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₃ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₃))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₃ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₃))
tt)
(λ n₄
`Arg A (λ _ `Rec n₄ (`End (con (there here , n₄ , refl)))))
, tt)
t₂))
m)
(λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t₁))
n₂)
n₁)
All
(case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₂
`Arg
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t₁))
m)
(λ _ `Rec n₂ (`End (con (there here , n₂ , refl)))))
, tt)
t)
(λ n₂ xss
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t₁))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
(λ u _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ u t,c₁
case
(λ t₁
(c₁
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
u c₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
((λ q ih
elimEq tt
(λ u₁ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₃ con (here , refl)) u q)
,
(λ n,q ih,tt
elimEq tt
(λ u₁ q
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₃
ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ u₁ t,c₂
case
(λ t₁
(c₁
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂)))
u₁)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(λ u₂ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
u₁ c₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
((λ q ih
elimEq tt
(λ u₂ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₄ n₄) u₁ q)
,
(λ n,q₁ ih,tt₁
elimEq tt
(λ u₂ q
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₄ con (there here , proj₁ ih,tt₁ n₄ , refl)) u₁ (proj₂ n,q₁))
, tt)
(proj₁ t,c₂) (proj₂ t,c₂))
n₃ (proj₁ ih,tt n₃))
u (proj₂ n,q))
, tt)
(proj₁ t,c₁) (proj₂ t,c₁))
n₂ m))
n₁ c
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₂
`Arg A (λ _ `Rec n₂ (`End (con (there here , n₂ , refl)))))
, tt)
t₁))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
(λ u _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ u t,c₁
case
(λ t₁
(c₁
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
u c₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
((λ q ih
elimEq tt
(λ u₁ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₂ con (here , refl)) u q)
,
(λ n,q ih,tt
elimEq tt
(λ u₁ q
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₂
ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ u₁ t,c₂
case
(λ t₁
(c₁
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂)))
u₁)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(λ u₂ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
u₁ c₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
((λ q ih
elimEq tt
(λ u₂ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₃ n₃) u₁ q)
,
(λ n,q₁ ih,tt₁
elimEq tt
(λ u₂ q
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₃ con (there here , proj₁ ih,tt₁ n₃ , refl)) u₁ (proj₂ n,q₁))
, tt)
(proj₁ t,c₂) (proj₂ t,c₂))
n₂ (proj₁ ih,tt n₂))
u (proj₂ n,q))
, tt)
(proj₁ t,c₁) (proj₂ t,c₁))
n₁ m))
((λ q ih
elimEq (con (here , refl))
(λ n₂ q₁
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ u _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u t,c₁
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
u c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
((λ q₂ ih₁
elimEq tt
(λ u₁ q₃
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₃ con (here , refl)) u q₂)
,
(λ n,q ih,tt
elimEq tt
(λ u₁ q₂
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₃
ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u₁ t,c₂
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u₁)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₂ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
u₁ c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
((λ q₂ ih₁
elimEq tt
(λ u₂ q₃
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₄ n₄) u₁ q₂)
,
(λ n,q₁ ih,tt₁
elimEq tt
(λ u₂ q₂
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₄ con (there here , proj₁ ih,tt₁ n₄ , refl)) u₁ (proj₂ n,q₁))
, tt)
(proj₁ t,c₂) (proj₂ t,c₂))
n₃ (proj₁ ih,tt n₃))
u (proj₂ n,q))
, tt)
(proj₁ t,c₁) (proj₂ t,c₁))
n₂ m))
(con (here , refl)) n₁ q)
,
(λ n',x,xs,q ih,tt
elimEq (con (there here , proj₁ n',x,xs,q , refl))
(λ n₂ q
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ u _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u t,c₁
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
u c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
((λ q₁ ih
elimEq tt
(λ u₁ q₂
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₃ con (here , refl)) u q₁)
,
(λ n,q ih,tt₁
elimEq tt
(λ u₁ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₃
ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u₁ t,c₂
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u₁)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₂ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
u₁ c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
((λ q₁ ih
elimEq tt
(λ u₂ q₂
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₄ n₄) u₁ q₁)
,
(λ n,q₁ ih,tt₂
elimEq tt
(λ u₂ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₄ con (there here , proj₁ ih,tt₂ n₄ , refl)) u₁ (proj₂ n,q₁))
, tt)
(proj₁ t,c₂) (proj₂ t,c₂))
n₃ (proj₁ ih,tt₁ n₃))
u (proj₂ n,q))
, tt)
(proj₁ t,c₁) (proj₂ t,c₁))
n₂ m))
(ind
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₂
`Arg A (λ _ `Rec n₂ (`End (con (there here , n₂ , refl)))))
, tt)
t))
(λ m₁ xs
(n₂
: μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t))
n₂
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ u _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u t,c₁
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
u c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
((λ q ih
elimEq tt
(λ u₁ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₃ n₃) u q)
,
(λ n,q ih,tt₁
elimEq tt
(λ u₁ q
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₃ con (there here , proj₁ ih,tt₁ n₃ , refl)) u (proj₂ n,q))
, tt)
(proj₁ t,c₁) (proj₂ t,c₁))
m₁ n₂))
(λ n₂ t,c₁
case
(λ t
(c
: El
(case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t)
(λ n₃
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₄
`Arg A (λ _ `Rec n₄ (`End (con (there here , n₄ , refl)))))
, tt)
t₁))
n₃)
n₂)
All
(case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t)
(λ m₁ xs
(n₃
: μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₄
`Arg A (λ _ `Rec n₄ (`End (con (there here , n₄ , refl)))))
, tt)
t₁))
n₃
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₄
`Arg A (λ _ `Rec n₄ (`End (con (there here , n₄ , refl)))))
, tt)
t₁))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
(λ u _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ u t,c₂
case
(λ t₁
(c₁
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
u c₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
((λ q ih
elimEq tt
(λ u₁ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₄ n₄) u q)
,
(λ n,q ih,tt₁
elimEq tt
(λ u₁ q
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₄ con (there here , proj₁ ih,tt₁ n₄ , refl)) u (proj₂ n,q))
, tt)
(proj₁ t,c₂) (proj₂ t,c₂))
m₁ n₃))
n₂ c
(n₃
: μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₄
`Arg A (λ _ `Rec n₄ (`End (con (there here , n₄ , refl)))))
, tt)
t₁))
n₃
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₄
`Arg A (λ _ `Rec n₄ (`End (con (there here , n₄ , refl)))))
, tt)
t₁))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
(λ u _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ u t,c₂
case
(λ t₁
(c₁
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
u c₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
((λ q ih
elimEq tt
(λ u₁ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₄ n₄) u q)
,
(λ n,q ih,tt₁
elimEq tt
(λ u₁ q
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₄ con (there here , proj₁ ih,tt₁ n₄ , refl)) u (proj₂ n,q))
, tt)
(proj₁ t,c₂) (proj₂ t,c₂))
n₂ n₃))
((λ q ih
elimEq (con (here , refl))
(λ n₃ q₁
(n₄
: μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₅
`Arg A (λ _ `Rec n₅ (`End (con (there here , n₅ , refl)))))
, tt)
t))
n₄
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₅
`Arg A (λ _ `Rec n₅ (`End (con (there here , n₅ , refl)))))
, tt)
t))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ u _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u t,c₂
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
u c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
((λ q₂ ih₁
elimEq tt
(λ u₁ q₃
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₅ n₅) u q₂)
,
(λ n,q ih,tt₁
elimEq tt
(λ u₁ q₂
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₅ con (there here , proj₁ ih,tt₁ n₅ , refl)) u (proj₂ n,q))
, tt)
(proj₁ t,c₂) (proj₂ t,c₂))
n₃ n₄))
(λ n₃ ys ys) n₂ q)
,
(λ n',x,xs,q₁ ih,tt₁
elimEq (con (there here , proj₁ n',x,xs,q₁ , refl))
(λ n₃ q
(n₄
: μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₅
`Arg A (λ _ `Rec n₅ (`End (con (there here , n₅ , refl)))))
, tt)
t))
n₄
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₅
`Arg A (λ _ `Rec n₅ (`End (con (there here , n₅ , refl)))))
, tt)
t))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ u _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u t,c₂
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
u c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
((λ q₁ ih
elimEq tt
(λ u₁ q₂
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₅ n₅) u q₁)
,
(λ n,q ih,tt₂
elimEq tt
(λ u₁ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₅ con (there here , proj₁ ih,tt₂ n₅ , refl)) u (proj₂ n,q))
, tt)
(proj₁ t,c₂) (proj₂ t,c₂))
n₃ n₄))
(λ n₃ ys
con
(there here ,
ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ u _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u t,c₂
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
u c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
((λ q ih
elimEq tt
(λ u₁ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₄ n₄) u q)
,
(λ n,q ih,tt₂
elimEq tt
(λ u₁ q
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₄ con (there here , proj₁ ih,tt₂ n₄ , refl)) u (proj₂ n,q))
, tt)
(proj₁ t,c₂) (proj₂ t,c₂))
(proj₁ n',x,xs,q₁) n₃
, proj₁ (proj₂ n',x,xs,q₁) , proj₁ ih,tt₁ n₃ ys , refl))
n₂ (proj₂ (proj₂ (proj₂ n',x,xs,q₁))))
, tt)
(proj₁ t,c₁) (proj₂ t,c₁))
(proj₁ (proj₂ n',x,xs,q))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ u _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u t,c₁
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
u c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
((λ q ih
elimEq tt
(λ u₁ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₂ con (here , refl)) u q)
,
(λ n,q ih,tt₁
elimEq tt
(λ u₁ q
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₂
ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ u₁ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u₁ t,c₂
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u₁)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₂ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
u₁ c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
((λ q ih
elimEq tt
(λ u₂ q₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₃ n₃) u₁ q)
,
(λ n,q₁ ih,tt₂
elimEq tt
(λ u₂ q
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ n₃ con (there here , proj₁ ih,tt₂ n₃ , refl)) u₁ (proj₂ n,q₁))
, tt)
(proj₁ t,c₂) (proj₂ t,c₂))
n₂ (proj₁ ih,tt₁ n₂))
u (proj₂ n,q))
, tt)
(proj₁ t,c₁) (proj₂ t,c₁))
(proj₁ n',x,xs,q) m)
(proj₁ ih,tt))
n₁ (proj₂ (proj₂ (proj₂ n',x,xs,q))))
, tt)
(proj₁ t,c) (proj₂ t,c))
λ A m n
ind
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₁
`Arg
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₂
`Arg A (λ _ `Rec n₂ (`End (con (there here , n₂ , refl)))))
, tt)
t₁))
m)
(λ _ `Rec n₁ (`End (con (there here , n₁ , refl)))))
, tt)
t))
(λ n₁ xss
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₂
`Arg A (λ _ `Rec n₂ (`End (con (there here , n₂ , refl)))))
, tt)
t))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ _ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u t,c
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₁ n₂
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₁)
u c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u)
((λ q ih n₂ con (here , refl)) ,
(λ m,q ih,tt n₂
ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ _ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u₁ t,c₁
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u₁)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₂ n₃
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₂
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₂)
u₁ c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₁)
((λ q ih n₃ n₃) ,
(λ m,q₁ ih,tt₁ n₃ con (there here , proj₁ ih,tt₁ n₃ , refl)) ,
tt)
(proj₁ t,c₁) (proj₂ t,c₁))
n₂ (proj₁ ih,tt n₂))
, tt)
(proj₁ t,c) (proj₂ t,c))
n₁ m))
(λ n₁ t,c
case
(λ t
(c
: El
(case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₂
`Arg
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t₁))
m)
(λ _ `Rec n₂ (`End (con (there here , n₂ , refl)))))
, tt)
t)
(λ n₂
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₃
`Arg
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₂
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₃ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₃))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₃ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₃))
tt)
(λ n₄
`Arg A (λ _ `Rec n₄ (`End (con (there here , n₄ , refl)))))
, tt)
t₂))
m)
(λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t₁))
n₂)
n₁)
All
(case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₂
`Arg
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t₁))
m)
(λ _ `Rec n₂ (`End (con (there here , n₂ , refl)))))
, tt)
t)
(λ n₂ xss
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t₁))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
(λ _ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ u t,c₁
case
(λ t₁
(c₁
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(λ u₁ n₃
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u₁)
u c₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u)
((λ q ih n₃ con (here , refl)) ,
(λ m,q ih,tt n₃
ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
(λ _ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ u₁ t,c₂
case
(λ t₁
(c₁
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂)))
u₁)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(λ u₂ n₄
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u₂
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u₂)
u₁ c₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u₁)
((λ q ih n₄ n₄) ,
(λ m,q₁ ih,tt₁ n₄ con (there here , proj₁ ih,tt₁ n₄ , refl)) ,
tt)
(proj₁ t,c₂) (proj₂ t,c₂))
n₃ (proj₁ ih,tt n₃))
, tt)
(proj₁ t,c₁) (proj₂ t,c₁))
n₂ m))
n₁ c
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₂
`Arg A (λ _ `Rec n₂ (`End (con (there here , n₂ , refl)))))
, tt)
t₁))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
(λ _ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ u t,c₁
case
(λ t₁
(c₁
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(λ u₁ n₂
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u₁)
u c₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u)
((λ q ih n₂ con (here , refl)) ,
(λ m,q ih,tt n₂
ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
(λ _ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ u₁ t,c₂
case
(λ t₁
(c₁
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂)))
u₁)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)
(λ u₂ n₃
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u₂
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u₂)
u₁ c₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
u₁)
((λ q ih n₃ n₃) ,
(λ m,q₁ ih,tt₁ n₃ con (there here , proj₁ ih,tt₁ n₃ , refl)) ,
tt)
(proj₁ t,c₂) (proj₂ t,c₂))
n₂ (proj₁ ih,tt n₂))
, tt)
(proj₁ t,c₁) (proj₂ t,c₁))
n₁ m))
((λ q ih
subst
(λ n₂
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ _ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u t,c₁
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₁ n₃
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₁)
u c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u)
((λ q₁ ih₁ n₃ con (here , refl)) ,
(λ m,q ih,tt n₃
ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ _ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u₁ t,c₂
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u₁)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₂ n₄
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₂
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₂)
u₁ c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₁)
((λ q₁ ih₁ n₄ n₄) ,
(λ m,q₁ ih,tt₁ n₄ con (there here , proj₁ ih,tt₁ n₄ , refl)) ,
tt)
(proj₁ t,c₂) (proj₂ t,c₂))
n₃ (proj₁ ih,tt n₃))
, tt)
(proj₁ t,c₁) (proj₂ t,c₁))
n₂ m))
q (con (here , refl)))
,
(λ n',xs,xss,q ih,tt
subst
(λ n₂
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ _ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u t,c₁
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₁ n₃
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₁)
u c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u)
((λ q ih n₃ con (here , refl)) ,
(λ m,q ih,tt₁ n₃
ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ _ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u₁ t,c₂
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u₁)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₂ n₄
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₂
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₂)
u₁ c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₁)
((λ q ih n₄ n₄) ,
(λ m,q₁ ih,tt₂ n₄ con (there here , proj₁ ih,tt₂ n₄ , refl)) ,
tt)
(proj₁ t,c₂) (proj₂ t,c₂))
n₃ (proj₁ ih,tt₁ n₃))
, tt)
(proj₁ t,c₁) (proj₂ t,c₁))
n₂ m))
(proj₂ (proj₂ (proj₂ n',xs,xss,q)))
(ind
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₂
`Arg A (λ _ `Rec n₂ (`End (con (there here , n₂ , refl)))))
, tt)
t))
(λ m₁ xs
(n₂
: μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t))
n₂
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t))
(ind
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
(λ _ _
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t))
tt)
(λ u t,c₁
case
(λ t
(c
: El (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁
case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁)))
u)
All (case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t)
(λ u₁ n₃
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₁
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u₁)
u c
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u
μ
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
u)
((λ q ih n₃ n₃) ,
(λ m,q ih,tt₁ n₃ con (there here , proj₁ ih,tt₁ n₃ , refl)) , tt)
(proj₁ t,c₁) (proj₂ t,c₁))
m₁ n₂))
(λ m₁ t,c₁
case
(λ t
(c
: El
(case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₁ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
tt)
(λ n₂
`Arg A (λ _ `Rec n₂ (`End (con (there here , n₂ , refl)))))
, tt)
t)
(λ n₂
μ
(`Arg (Tag ("nil""cons" ∷ []))
(λ t₁
case
(λ _
Desc
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt))
(`End (con (here , refl)) ,
`Arg
(`Arg (Tag ("zero""suc" ∷ []))
(λ t₂ case (λ _ Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₂))
tt)
(λ n₃
`Arg A (λ _ `Rec n₃ (`End (con (there here , n₃ , refl)))))
, tt)
t₁))
n₂)
m₁)
All
(case
(λ _
Desc