proposition: Lemma toto' : [ {f : A -> B | forall z, z <> x -> f z = y} ].
proof: Proof. destruct (AC A (fun z => {r | r = y})) as [f]. intro. constructor. eauto. constructor. pose (g := fun z => proj1_sig (f z)). exists g. intros z Hz. unfold g. destruct (f z). auto. Qed.
imports: Monad Examples