English
A second auxiliary relation shows compatibility between foldr' and the next-layer foldr'Aux, ensuring coherence of the two-tier recursion for all generators m and x.
Русский
Вторая вспомогательная связка демонстрирует совместимость между foldr' и foldr'Aux, обеспечивая согласованность двухуровневой рекурсии по всем генераторам m и x.
LaTeX
$$$foldr'Aux\\ Q\\ f\\ hf\\ n\\ (ι_Q m) = f m (1, n)$$$
Lean4
theorem foldr'_ι (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N) (hf : ∀ m x fx, f m (ι Q m * x, f m (x, fx)) = Q m • fx)
(n m) : foldr' Q f hf n (ι Q m) = f m (1, n) :=
congr_arg Prod.snd (foldr_ι _ _ _ _ _)