proposition: Lemma covariant_tclosure : forall A (R1 R2 : binary A), rel_incl R1 R2 -> rel_incl (tclosure R1) (tclosure R2).
proof: Proof. Proof using. introv H M. induction* M. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)