no goals
F : PFunctor
X : Type ?u.26665
f : X → Obj F X
a : F.A
x : B F a → M F
i : B F (head (M.mk { fst := a, snd := x }))
⊢ B F (head (M.mk { fst := a, snd := x })) = B F a
rw [head_mk]
case H
F : PFunctor
X : Type ?u.26665
f : X → Obj F X
a : F.A
x : B F a → M F
i : B F (head (M.mk { fst := a, snd := x }))
⊢ ∀ (i_1 : ℕ),
    MIntl.approx (children (M.mk { fst := a, snd := x }) i) i_1 =
      MIntl.approx (x (cast (_ : B F (head (M.mk { fst := a, snd := x })) = B F a) i)) i_1
F : PFunctor
X : Type ?u.26665
f : X → Obj F X
a : F.A
x : B F a → M F
i : B F (head (M.mk { fst := a, snd := x }))
⊢ children (M.mk { fst := a, snd := x }) i = x (cast (_ : B F (head (M.mk { fst := a, snd := x })) = B F a) i)
apply ext'
case H
F : PFunctor
X : Type ?u.26665
f : X → Obj F X
a : F.A
x : B F a → M F
i : B F (head (M.mk { fst := a, snd := x }))
n : ℕ
⊢ MIntl.approx (children (M.mk { fst := a, snd := x }) i) n =
    MIntl.approx (x (cast (_ : B F (head (M.mk { fst := a, snd := x })) = B F a) i)) n
case H
F : PFunctor
X : Type ?u.26665
f : X → Obj F X
a : F.A
x : B F a → M F
i : B F (head (M.mk { fst := a, snd := x }))
⊢ ∀ (i_1 : ℕ),
    MIntl.approx (children (M.mk { fst := a, snd := x }) i) i_1 =
      MIntl.approx (x (cast (_ : B F (head (M.mk { fst := a, snd := x })) = B F a) i)) i_1
intro n
no goals
case H
F : PFunctor
X : Type ?u.26665
f : X → Obj F X
a : F.A
x : B F a → M F
i : B F (head (M.mk { fst := a, snd := x }))
n : ℕ
⊢ MIntl.approx (children (M.mk { fst := a, snd := x }) i) n =
    MIntl.approx (x (cast (_ : B F (head (M.mk { fst := a, snd := x })) = B F a) i)) n
rfl