proposition: Lemma tc1_eq A (R : rel A) x y : R!1 x y <-> R! x y.
proof: Proof. split; induction 1. apply t_step. hyp. trans y. apply t_step. hyp. hyp. apply t1_step. hyp. trans y; hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)