proposition: Lemma ec_min A (R S : rel A) : Equivalence S -> R << S -> clos_equiv R << S.
proof: Proof. intros S_eq RS. intros u v; revert u v; induction 1. fo. refl. trans y; hyp. hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)