proposition: Lemma g_def : forall beta, In B beta -> _A beta = members (g beta ).
proof: Proof. intros. pattern (g beta); unfold g; apply iota_ind. - case (g_def1 H); intros a' [Ha' Ha'']; exists a'; split;auto. intros x (Hx,H'x); eapply g_unic;eauto. - now intros x ((Hx,H'x),U). Qed.
imports: ZornsLemma(CountableTypes)