proposition: Lemma tc_eq A (R S : rel A) : S << R -> R << S! -> R! == S!.
proof: Proof. intros SR RSt. split; apply tc_min. hyp. apply tc_trans. trans R. hyp. apply incl_tc. refl. apply tc_trans. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)