proposition: Lemma surjective_inverse_axioms : forall (a b : E) (f : E1), surjective a b f -> axioms b a (inverse a f).
proof: Proof. ir. unfold axioms in |- *. ir. unfold inverse in |- *. unfold surjective in H; xd. unfold covers in H1; xd. pose (H1 x H0). pose (choose_pr e). assert (A (inc (choose (fun x0 : E => A (inc x0 a) (f x0 = x))) a) (f (choose (fun x0 : E => A (inc x0 a) (f x0 = x))) = x)). am. xd. Qed.
imports: set_theory