Skip to content

Instantly share code, notes, and snippets.

@larrytheliquid

larrytheliquid/InferredPropositionalDescEliminatorConcat.agda

Last active January 3, 2016 10:09
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₃ →
μ
(`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)