proposition: Lemma sub_domain : forall f g : E, sub f g -> sub (domain f) (domain g).
proof: Proof. ir. unfold sub in |- *. unfold domain in |- *. unfold sub in H. ir. set (K := Image.ex H0) in *. nin K. nin H1. rewrite <- H2. ap Image.incl. au. Qed.
imports: set_theory