English
An AList built by consing a new element c onto l is equal to inserting c into the AList formed by l with its nodupKeys adjusted accordingly.
Русский
AList, построенный добавлением элемента c перед списком l, равен вставке элемента c в AList, полученный из l с изменением nodupKeys.
LaTeX
$$$ (\langle c :: l, h \rangle : AList \beta) = insert c.1 c.2 \langle l, nodupKeys_of_nodupKeys_cons h \rangle $$$
Lean4
theorem mk_cons_eq_insert (c : Sigma β) (l : List (Sigma β)) (h : (c :: l).NodupKeys) :
(⟨c :: l, h⟩ : AList β) = insert c.1 c.2 ⟨l, nodupKeys_of_nodupKeys_cons h⟩ := by
simpa [insert] using (kerase_of_notMem_keys <| notMem_keys_of_nodupKeys_cons h).symm
