proposition: Lemma Forall2_transitive {C} (Q : B → C → Prop) (R : A → C → Prop) l k lC : (∀ x y z, P x y → Q y z → R x z) → Forall2 P l k → Forall2 Q k lC → Forall2 R l lC.
proof: Proof. intros ? Hl. revert lC. induction Hl; inv 1; eauto. Qed.
imports: stdpp(options)