proposition: Lemma plus_assoc' (gamma : Ord) : alpha + (beta + gamma) = (alpha + beta) + gamma.
proof: Proof. intros; generalize plus_assoc3; unfold f_alpha_beta, g_alpha_beta. intros;symmetry;apply H. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)