Skip to content

Instantly share code, notes, and snippets.

@larrytheliquid

larrytheliquid/InferredPropositionalDescEliminatorConcat.agda

Last active Jan 3, 2016
Star
Embed
What would you like to do?
Learn more about clone URLs
Download ZIP
Canonical terms for the concat function in this blog post: http://spire-lang.org/blog/2014/01/15/modeling-elimination-of-described-types/
Raw
InferredPropositionalDescEliminatorConcat.agda
λ 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))
Raw
InferredPropositionalDescInductionConcat.agda
λ 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₃ →