no goals
F : PFunctor
X : Type ?u.28846
f✝ : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
a : F.A
f : B F a → M F
i : B F a
⊢ iselect ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) = iselect ps (f i)
simp only [iselect, isubtree_cons]