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