proposition: Lemma X_eq : forall (x : E) (f : x -> E) (y z : E), (exists a : x, A (R a = y) (f a = z)) -> X f y = z.
proof: Proof. ir. nin H. xd. unfold X in |- *. assert (inc y x). rewrite <- H. ap R_inc. apply Yy_if with H1. assert (B H1 = x0). ap R_inj. rewrite B_eq. au. rewrite H2. am. Qed.
imports: tactics