English
iselect on a cons path reduces to iselect on the tail: iselect (⟨a,i⟩ :: ps) (M.mk ⟨a,f⟩) = iselect ps (f i).
Русский
iselect для конуса пути эквивалентен iselect на хвосте: iselect (⟨a,i⟩ :: ps) (M.mk ⟨a,f⟩) = iselect ps (f i).
LaTeX
$$$\\operatorname{iselect} (\\langle a,i\\rangle :: ps)\\ (\\operatorname{M.mk}\\langle a,f\\rangle) = \\operatorname{iselect} ps (f\\ i)$$$
Lean4
@[simp]
theorem iselect_cons [DecidableEq F.A] [Inhabited (M F)] (ps : Path F) {a} (f : F.B a → M F) {i} :
iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = iselect ps (f i) := by simp only [iselect, isubtree_cons]