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