English
Another compatibility lemma asserting the equality of the recursor applied to a cons with the direct cons construction.
Русский
Ещё одно лемма совместимости: рекурсор применённый к cons равен прямому конструктору cons.
LaTeX
$$$\\mathrm{consRecOn\\,cons}\\ g\\ u\\ w = \\mathrm{cons}(g,u,w,h_1,h_2)\\, $$$
Lean4
@[simp]
theorem consRecOn_cons {motive : NormalWord d → Sort*} (g : G) (u : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u)
(h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u')
(ofGroup : ∀ g, motive (ofGroup g))
(cons :
∀ (g : G) (u : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u)
(h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'),
motive w → motive (cons g u w h1 h2)) :
consRecOn (.cons g u w h1 h2) ofGroup cons = cons g u w h1 h2 (consRecOn w ofGroup cons) :=
rfl
