proposition: Lemma record_pair_pr : forall (a : E) (f : E1) (x y : E), inc (pair x y) (record a f) -> (inc x a & inc y (f x)).
proof: Proof. ir. xd. pose (record_in H). unfold in_record in (type of i); xd. rewrite pr1_pair in H1. am. pose (record_in H). unfold in_record in (type of i); xd. rewrite pr1_pair in H2. rewrite pr2_pair in H2. am. Qed.
imports: set_theory