proposition: Lemma record_pair_inc : forall (a : E) (f : E1) (x y : E), inc x a -> inc y (f x) -> inc (pair x y) (record a f).
proof: Proof. ir. ap record_inc. unfold in_record in |- *; xd. ap pair_is_pair. rewrite pr1_pair; am. rewrite pr2_pair; rewrite pr1_pair; am. Qed.
imports: set_theory