case mk
F : PFunctor
y : M F
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H : ∀ (i : ℕ), MIntl.approx { approx := approx✝, consistent := consistent✝ } i = MIntl.approx y i
⊢ { approx := approx✝, consistent := consistent✝ } = y
F : PFunctor
x y : M F
H : ∀ (i : ℕ), MIntl.approx x i = MIntl.approx y i
⊢ x = y
cases x
case mk.mk
F : PFunctor
approx✝¹ : (n : ℕ) → CofixA F n
consistent✝¹ : AllAgree approx✝¹
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H :
  ∀ (i : ℕ),
    MIntl.approx { approx := approx✝¹, consistent := consistent✝¹ } i =
      MIntl.approx { approx := approx✝, consistent := consistent✝ } i
⊢ { approx := approx✝¹, consistent := consistent✝¹ } = { approx := approx✝, consistent := consistent✝ }
case mk
F : PFunctor
y : M F
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H : ∀ (i : ℕ), MIntl.approx { approx := approx✝, consistent := consistent✝ } i = MIntl.approx y i
⊢ { approx := approx✝, consistent := consistent✝ } = y
cases y
case mk.mk.e_approx.h
F : PFunctor
approx✝¹ : (n : ℕ) → CofixA F n
consistent✝¹ : AllAgree approx✝¹
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H :
  ∀ (i : ℕ),
    MIntl.approx { approx := approx✝¹, consistent := consistent✝¹ } i =
      MIntl.approx { approx := approx✝, consistent := consistent✝ } i
n : ℕ
⊢ approx✝¹ n = approx✝ n
case mk.mk
F : PFunctor
approx✝¹ : (n : ℕ) → CofixA F n
consistent✝¹ : AllAgree approx✝¹
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H :
  ∀ (i : ℕ),
    MIntl.approx { approx := approx✝¹, consistent := consistent✝¹ } i =
      MIntl.approx { approx := approx✝, consistent := consistent✝ } i
⊢ { approx := approx✝¹, consistent := consistent✝¹ } = { approx := approx✝, consistent := consistent✝ }
congr with n
no goals
case mk.mk.e_approx.h
F : PFunctor
approx✝¹ : (n : ℕ) → CofixA F n
consistent✝¹ : AllAgree approx✝¹
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H :
  ∀ (i : ℕ),
    MIntl.approx { approx := approx✝¹, consistent := consistent✝¹ } i =
      MIntl.approx { approx := approx✝, consistent := consistent✝ } i
n : ℕ
⊢ approx✝¹ n = approx✝ n
apply H