proposition: Lemma function_set_sub_powerset_record : forall (a : E) (f : E1), sub (function_set a f) (powerset (record a f)).
proof: Proof. ir. unfold sub in |- *; ir. pose (function_set_iff a f x). unfold iff in (type of i); xd. pose (H0 H). ap powerset_inc. ap in_fs_sub_record; au. Qed.
imports: set_theory