proposition: Lemma Forall2_rel_le : forall P Q r s, Forall2 P r s -> rel_incl P Q -> Forall2 Q r s.
proof: Proof. Proof using. introv F W. unfolds rel_incl, pred_incl. induction F; constructors~. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)