proposition: Lemma in_fs_for_L : forall (a : E) (f v : E1), (forall y : E, inc y a -> inc (v y) (f y)) -> in_function_set a f (Function.create a v).
proof: Proof. ir. unfold in_function_set in |- *; xd. ap Function.create_axioms. ap Function.create_domain. ir. rewrite Function.create_V_rewrite. ap H; au. am. Qed.
imports: set_theory