proposition: Lemma rel_incl_union_rstclosure : forall R1 R2, rel_incl (union (rstclosure R1) (rstclosure R2)) (rstclosure (union R1 R2)).
proof: Proof. Proof using. hint rel_incl_union_l, rel_incl_union_r. introv [M|M]. { applys* covariant_rstclosure R1. } { applys* covariant_rstclosure R2. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)