proposition: Lemma inter_covariant: forall A (E E' F F' : set A), E \c E' -> F \c F' -> (E \n F) \c (E' \n F').
proof: Proof. Proof using. set_prove. Qed.
imports: TLC(LibTactics) TLC(LibLogic LibEqual LibList LibRelation LibWf LibList LibLN)