proposition: Lemma in_record_ex : forall (a : E) (f : E1) (x : E), in_record a f x -> exists i : recordRec a f, recordMap i = x.
proof: Proof. ir. unfold in_record in H; xd. set (u := B H0). assert (R u = pr1 x). unfold u in |- *. ap B_eq. assert (inc (pr2 x) (f (R u))). rewrite H2; am. set (v := B H3). pose (Build_recordRec (a:=a) (f:=f) (first:=u) v). apply ex_intro with r. transitivity (pair (R u) (R v)). tv. assert (R v = pr2 x). unfold v in |- *. ap B_eq. rewrite H4. assert (R u = pr1 x); au. rewrite H5. ap pair_recov. am. Qed.
imports: set_theory