|
λ 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)) |
