no goals
F : PFunctor
X : Type ?u.26443
f : X → Obj F X
x : Obj F (M F)
⊢ x.fst = (dest (M.mk x)).fst
rw [dest_mk]
no goals
F : PFunctor
X : Type ?u.26443
f : X → Obj F X
x : Obj F (M F)
⊢ (dest (M.mk x)).fst = head (M.mk x)
rfl