Map M implies forall₂

public theorem mapM_implies_forall₂  {f : α → Except ε β}  {p : α → β → Prop}  {xs : List α} {ys : List β}  (h : ∀ x y, x ∈ xs → f x = .ok y → p x y)  (hmapM : List.mapM f xs = .ok ys) :  List.Forall₂ p xs ys:= by  induction xs generalizing ys  case nil =>    simp only [mapM, mapM.loop, pure, Except.pure, reverse_nil, Except.ok.injEq, nil_eq] at hmapM    simp [hmapM]  case cons xhd xtl ih =>    simp only [mapM_cons, Bind.bind, Except.bind, pure, Except.pure] at hmapM    split at hmapM    contradiction    split at hmapM    contradiction    simp only [Except.ok.injEq] at hmapM    simp only [← hmapM, forall₂_cons]    constructor    · apply h      simp only [mem_cons, true_or]      assumption    · apply ih      intros      apply h      simp only [mem_cons, or_true, *]      assumption      assumption