English
For f and lists as, bs with length bs ≤ length as, map₂Right f as bs equals zipWith (λ a b, f (Some a) b) as bs.
Русский
Для f и списков as, bs с условием length bs ≤ length as, выполняется map₂Right f as bs = zipWith (λ a b, f(Some a) b) as bs.
LaTeX
$$$\\forall f:\\alpha \\to \\mathrm{Option}\\,\\beta \\to \\gamma\\ ,\\ (\\mathrm{length}\\ bs \\le \\mathrm{length}\\ as) \\Rightarrow\\ \\mathrm{map₂Right}\\ f\\ as bs = \\mathrm{zipWith}(\\lambda a b. f(\\mathrm{Some}\\ a) b)\\ as\\ bs$$$
Lean4
theorem map₂Right_eq_zipWith (h : length bs ≤ length as) :
map₂Right f as bs = zipWith (fun a b => f (some a) b) as bs :=
by
have : (fun a b => flip f a (some b)) = flip fun a b => f (some a) b := rfl
simp only [map₂Right, map₂Left_eq_zipWith, zipWith_flip, *]
