γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ PEmpty.elim = f
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ ofList γ (toList γ (mk Listα.nil f)) = mk Listα.nil f
simp only [toList, ofList, mk.injEq, heq_eq_eq, true_and]
case h
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
x : PEmpty
⊢ PEmpty.elim x = f x
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ PEmpty.elim = f
ext x
no goals
case h
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
x : PEmpty
⊢ PEmpty.elim x = f x
cases x
γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
⊢ (fun x => f PUnit.unit) = f
γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
⊢ ofList γ (toList γ (mk (Listα.cons x) f)) = mk (Listα.cons x) f
simp only [ofList, leftInverse_list (f PUnit.unit), mk.injEq, heq_eq_eq, true_and]
no goals
γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
⊢ (fun x => f PUnit.unit) = f
rfl