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