proposition: Lemma prop_subrel A (R S : rel A) : Equivalence S -> subrelation R S -> Proper (R ==> R ==> impl) S.
proof: Proof. intros S_eq RS u u' uu' v v' vv' uv. apply RS in uu'. apply RS in vv'. rewrite <- uu', <- vv'. hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)