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