proposition: Lemma rtc1_eq A (R : rel A) x y : R#1 x y <-> R# x y.
proof: Proof. split; induction 1. refl. trans y. apply rt_step. hyp. hyp. eapply rt1_trans. apply H. refl. refl. trans y; hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)