proposition: Lemma union_inc : forall x y a : E, inc x y -> inc y a -> inc x (union a).
proof: Proof. ir. pose (B H0). assert (R a0 = y). unfold a0 in |- *. ap B_eq. assert (inc x (R a0)). rewrite H1. am. pose (B H2). pose (Build_Integral (x:=a) (param:=a0) r). unfold union in |- *. ap IM_inc. apply ex_intro with i. change (R r = x) in |- *. unfold r in |- *. ap B_eq. Qed.
imports: tactics