proposition: Lemma Forall2_forall `{Inhabited A} B C (Q : A → B → C → Prop) l k : Forall2 (λ x y, ∀ z, Q z x y) l k ↔ ∀ z, Forall2 (Q z) l k.
proof: Proof. split; [induction 1; constructor; auto|]. intros Hlk. induction (Hlk inhabitant) as [|x y l k _ _ IH]; constructor. - intros z. by oinv Hlk. - apply IH. intros z. by oinv Hlk. Qed.
imports: stdpp(options)