[GOAL]
f : Natβ Natα.zero → WType Natβ
⊢ ofNat (toNat (mk Natα.zero f)) = mk Natα.zero f
[PROOFSTEP]
rw [toNat, ofNat]
[GOAL]
f : Natβ Natα.zero → WType Natβ
⊢ mk Natα.zero Empty.elim = mk Natα.zero f
[PROOFSTEP]
congr
[GOAL]
case e_f
f : Natβ Natα.zero → WType Natβ
⊢ Empty.elim = f
[PROOFSTEP]
ext x
[GOAL]
case e_f.h
f : Natβ Natα.zero → WType Natβ
x : Empty
⊢ Empty.elim x = f x
[PROOFSTEP]
cases x
[GOAL]
f : Natβ Natα.succ → WType Natβ
⊢ ofNat (toNat (mk Natα.succ f)) = mk Natα.succ f
[PROOFSTEP]
simp only [toNat, ofNat, leftInverse_nat (f ()), mk.injEq, heq_eq_eq, true_and]
[GOAL]
f : Natβ Natα.succ → WType Natβ
⊢ (fun x => f ()) = f
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ toNat (ofNat (Nat.succ n)) = Nat.succ n
[PROOFSTEP]
rw [ofNat, toNat, rightInverse_nat n]
[GOAL]
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ ofList γ (toList γ (mk Listα.nil f)) = mk Listα.nil f
[PROOFSTEP]
simp only [toList, ofList, mk.injEq, heq_eq_eq, true_and]
[GOAL]
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ PEmpty.elim = f
[PROOFSTEP]
ext x
[GOAL]
case h
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
x : PEmpty
⊢ PEmpty.elim x = f x
[PROOFSTEP]
cases x
[GOAL]
γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
⊢ ofList γ (toList γ (mk (Listα.cons x) f)) = mk (Listα.cons x) f
[PROOFSTEP]
simp only [ofList, leftInverse_list (f PUnit.unit), mk.injEq, heq_eq_eq, true_and]
[GOAL]
γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
⊢ (fun x => f PUnit.unit) = f
[PROOFSTEP]
rfl
[GOAL]
γ : Type u
hd : γ
tl : List γ
⊢ toList γ (ofList γ (hd :: tl)) = hd :: tl
[PROOFSTEP]
simp only [toList, rightInverse_list tl]
