proposition: Lemma subset : forall a b x y, sub x y -> (forall u, inc u x -> a u = b u) -> sub (Image.create x a) (Image.create y b).
proof: Proof. ir. uhg; ir. rwi Image.inc_rw H1. nin H1; ee. rw Image.inc_rw. sh x1; xd. wr H2; sy; ap H0; am. Qed.
imports: tactics