proposition: Lemma tc_transp A (R : rel A) : transp (R!) == (transp R)!.
proof: Proof. intros; split; compute. induction 1. constructor; trivial. constructor 2 with y; auto. induction 1. constructor; trivial. constructor 2 with y; auto. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)