proposition: Lemma union_exists : forall x a : E, inc x (union a) -> ex (fun y : E => A (inc x y) (inc y a)).
proof: Proof. ir. unfold union in H. pose (IM_exists H). nin e. apply ex_intro with (R (param x0)). xd. rewrite <- H0. ap R_inc. ap R_inc. Qed.
imports: tactics