proposition: Lemma prop2_incl A B C (f : A -> B -> C) : Proper (incl --> incl --> incl ==> impl) (fun R S T => Proper (R ==> S ==> T) f).
proof: Proof. intros R R' RR' S S' SS' T T' TT' hf x x' xx' y y' yy'. apply TT'. apply hf; fo. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)