proposition: Lemma same : forall (a b:E1) (x y:E), x = y -> (forall u, inc u x -> a u = b u) -> Image.create x a = Image.create y b.
proof: Proof. ir. ap extensionality. ap subset. rw H; uhg; ir; am. am. ap subset. rw H; uhg; ir; am. ir. sy; ap H0. rw H; am. Qed.
imports: tactics