case mk
P : PFunctor
α β : Type u
a✝ : P.A
f✝ : B P a✝ → WType P.B
⊢ mk (dest (WType.mk a✝ f✝)) = WType.mk a✝ f✝
P : PFunctor
α β : Type u
p : W P
⊢ mk (dest p) = p
cases p
no goals
case mk
P : PFunctor
α β : Type u
a✝ : P.A
f✝ : B P a✝ → WType P.B
⊢ mk (dest (WType.mk a✝ f✝)) = WType.mk a✝ f✝
rfl