proposition: Lemma covariant_union : forall R1 R2 S1 S2, rel_incl R1 S1 -> rel_incl R2 S2 -> rel_incl (union R1 R2) (union S1 S2).
proof: Proof. Proof using. unfold rel_incl, union. autos*. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)