English
A convenience form of InsertRec InsertMk: applying insertRec with a pair (a,b) inserted into l is equal to IH applied to that pair and the rest.
Русский
Упрощённая форма: вставка пары (a,b) в список l в обход InsertRec равна IH применённому к этой паре и остальному списку.
LaTeX
$$$ @insertRec \ α β _ C H0 IH ( l.insert a b ) = IH a b l h ( @insertRec α β _ C H0 IH l ) $$$
Lean4
theorem insertRec_insert_mk {C : AList β → Sort*} (H0 : C ∅)
(IH : ∀ (a : α) (b : β a) (l : AList β), a ∉ l → C l → C (l.insert a b)) {a : α} (b : β a) {l : AList β}
(h : a ∉ l) : @insertRec α β _ C H0 IH (l.insert a b) = IH a b l h (@insertRec α β _ C H0 IH l) :=
@insertRec_insert α β _ C H0 IH ⟨a, b⟩ l h
