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 _. unfold g; destruct (f z); auto. Qed.
imports: Monad Examples