proposition: Lemma image_covariant : forall A B (f : A -> B) (E F : set A), E \c F -> image f E \c image f F.
proof: Proof. Proof using. introv. do 2 rewrite incl_in_eq. introv M N. lets (y&Hy&Ey): in_image_inv (rm N). applys* in_image_prove. Qed.
imports: TLC(LibTactics LibLogic LibContainer LibSet)