proposition: Lemma in_fs_eq_L : forall (a : E) (f : E1) (u : E), in_function_set a f u -> u = Function.create a (fun y : E => V y u).
proof: Proof. ir. unfold in_function_set in H; xd. rewrite <- H0. sy. ap Function.create_recovers. am. Qed.
imports: set_theory