f : Natβ Natα.zero → WType Natβ
⊢ mk Natα.zero Empty.elim = mk Natα.zero f
f : Natβ Natα.zero → WType Natβ
⊢ ofNat (toNat (mk Natα.zero f)) = mk Natα.zero f
rw [toNat, ofNat]
case e_f
f : Natβ Natα.zero → WType Natβ
⊢ Empty.elim = f
f : Natβ Natα.zero → WType Natβ
⊢ mk Natα.zero Empty.elim = mk Natα.zero f
congr
case e_f.h
f : Natβ Natα.zero → WType Natβ
x : Empty
⊢ Empty.elim x = f x
case e_f
f : Natβ Natα.zero → WType Natβ
⊢ Empty.elim = f
ext x
no goals
case e_f.h
f : Natβ Natα.zero → WType Natβ
x : Empty
⊢ Empty.elim x = f x
cases x
f : Natβ Natα.succ → WType Natβ
⊢ (fun x => f ()) = f
f : Natβ Natα.succ → WType Natβ
⊢ ofNat (toNat (mk Natα.succ f)) = mk Natα.succ f
simp only [toNat, ofNat, leftInverse_nat (f ()), mk.injEq, heq_eq_eq, true_and]
no goals
f : Natβ Natα.succ → WType Natβ
⊢ (fun x => f ()) = f
rfl