proposition: Remark restrict : fun_bijection U M f.
proof: Proof. split. - destruct 1;auto. - red; case fbij. intros H H0 H1 b H2; case (H0 b). + apply inc;auto. + intros x (Hx,H'x); exists x;split;auto. red;unfold U; split;auto. subst b;auto. - red; destruct 1. destruct 1. intros H3; case fbij;intros; now apply H6. Qed.
imports: ZornsLemma(CountableTypes)