proposition: Lemma domain_tack_on : forall f x y:E, domain (tack_on f (pair x y)) = tack_on (domain f) x.
proof: Proof. ir. ap extensionality; uhg; ir. ufi domain H; rwi Image.inc_rw H; nin H; ee. rwi tack_on_inc H; nin H. rw tack_on_inc; ap or_introl. uf domain; rw Image.inc_rw. sh x1. xd. rw tack_on_inc; ap or_intror. wr H0; rw H. rw pr1_pair. tv. uf domain; rw Image.inc_rw. rwi tack_on_inc H; nin H. ufi domain H; rwi Image.inc_rw H; nin H; ee. sh x1. ee; try am. rw tack_on_inc. ap or_introl;am. sh (pair x y). ee. rw tack_on_inc; ap or_intror; tv. rw pr1_pair. sy; am. Qed.
imports: set_theory