case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
a✝ : (P F).A
f✝ : PFunctor.B (P F) a✝ → WType (P F).B
⊢ recF g (WType.mk a✝ f✝) = g (abs (recF g <$> PFunctor.W.dest (WType.mk a✝ f✝)))
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x : PFunctor.W (P F)
⊢ recF g x = g (abs (recF g <$> PFunctor.W.dest x))
cases x
no goals
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
a✝ : (P F).A
f✝ : PFunctor.B (P F) a✝ → WType (P F).B
⊢ recF g (WType.mk a✝ f✝) = g (abs (recF g <$> PFunctor.W.dest (WType.mk a✝ f✝)))
rfl