case intro
F : PFunctor
n : ℕ
a✝¹ : F.A
a✝ : B F a✝¹ → CofixA F (Nat.add n 0)
⊢ CofixA.intro a✝¹ a✝ = CofixA.intro (head' (CofixA.intro a✝¹ a✝)) (children' (CofixA.intro a✝¹ a✝))
F : PFunctor
n : ℕ
x : CofixA F (n + 1)
⊢ x = CofixA.intro (head' x) (children' x)
cases x
no goals
case intro
F : PFunctor
n : ℕ
a✝¹ : F.A
a✝ : B F a✝¹ → CofixA F (Nat.add n 0)
⊢ CofixA.intro a✝¹ a✝ = CofixA.intro (head' (CofixA.intro a✝¹ a✝)) (children' (CofixA.intro a✝¹ a✝))
rfl