case intro
F : PFunctor
n : ℕ
a✝ : F.A
x✝ : B F a✝ → CofixA F n
x'✝ : B F a✝ → CofixA F (n + 1)
hagree : ∀ (i : B F a✝), Agree (x✝ i) (x'✝ i)
i : B F (head' (CofixA.intro a✝ x✝))
j : B F (head' (CofixA.intro a✝ x'✝))
h₀ : HEq i j
⊢ Agree (children' (CofixA.intro a✝ x✝) i) (children' (CofixA.intro a✝ x'✝) j)
F : PFunctor
n : ℕ
x : CofixA F (succ n)
y : CofixA F (succ n + 1)
i : B F (head' x)
j : B F (head' y)
h₀ : HEq i j
h₁ : Agree x y
⊢ Agree (children' x i) (children' y j)
cases' h₁ with _ _ _ _ _ _ hagree
case intro.refl
F : PFunctor
n : ℕ
a✝ : F.A
x✝ : B F a✝ → CofixA F n
x'✝ : B F a✝ → CofixA F (n + 1)
hagree : ∀ (i : B F a✝), Agree (x✝ i) (x'✝ i)
i : B F (head' (CofixA.intro a✝ x✝))
⊢ Agree (children' (CofixA.intro a✝ x✝) i) (children' (CofixA.intro a✝ x'✝) i)
case intro
F : PFunctor
n : ℕ
a✝ : F.A
x✝ : B F a✝ → CofixA F n
x'✝ : B F a✝ → CofixA F (n + 1)
hagree : ∀ (i : B F a✝), Agree (x✝ i) (x'✝ i)
i : B F (head' (CofixA.intro a✝ x✝))
j : B F (head' (CofixA.intro a✝ x'✝))
h₀ : HEq i j
⊢ Agree (children' (CofixA.intro a✝ x✝) i) (children' (CofixA.intro a✝ x'✝) j)
cases h₀
no goals
case intro.refl
F : PFunctor
n : ℕ
a✝ : F.A
x✝ : B F a✝ → CofixA F n
x'✝ : B F a✝ → CofixA F (n + 1)
hagree : ∀ (i : B F a✝), Agree (x✝ i) (x'✝ i)
i : B F (head' (CofixA.intro a✝ x✝))
⊢ Agree (children' (CofixA.intro a✝ x✝) i) (children' (CofixA.intro a✝ x'✝) i)
apply hagree