proposition: Lemma in_fs_sub_record : forall (a : E) (f : E1) (u : E), in_function_set a f u -> sub u (record a f).
proof: Proof. ir. unfold in_function_set in H; xd. unfold sub in |- *; ir. pose (Function.pr2_V H H2). assert (Function.axioms u). am. unfold Function.axioms in H3; xd. pose (H3 _ H2). rewrite <- e0. ap record_pair_inc. rewrite <- H0. ap Function.lem2; au. rewrite e. ap H1. rewrite <- H0. ap Function.lem2; au. Qed.
imports: set_theory