English
For any f and elements a, as, b, bs, map₂Right' f (a :: as) (b :: bs) equals let r := map₂Right' f as bs in (f (Some a) b :: r.fst, r.snd).
Русский
Для любого f и элементов a, as, b, bs выполняется map₂Right' f (a :: as) (b :: bs) = let r := map₂Right' f as bs в (f (Some a) b :: r.fst, r.snd).
LaTeX
$$$\\forall f:\\alpha \\to \\mathrm{Option}\\,\\alpha \\to \\gamma\\ ,\\ \\text{map₂Right}'\\ f\\ (a::as)\\ (b::bs) =\\; \\text{let } r := \\text{map₂Right}'\\ f\\ as\\ bs \\text{ in }(f(\\mathrm{Some}\\ a)\\ b :: r.fst, r.snd)$$$
Lean4
@[simp]
theorem map₂Right'_cons_cons :
map₂Right' f (a :: as) (b :: bs) =
let r := map₂Right' f as bs
(f (some a) b :: r.fst, r.snd) :=
rfl
