proposition: Theorem cnf_exists (alpha : Ord) : exists l: cnf_t, is_cnf_of alpha l.
proof: Proof. case (le_eq_or_lt (zero_le alpha)). - exists nil; split. + constructor. + simpl;auto. - pattern alpha; apply transfinite_induction;auto. intros a H0 H1; case (classic (AP a)). + intros H2; apply cnf_of_ap; auto. + intros H2; case (not_AP_inv2 H1 H2). intros x H3; destruct H3 as [z [H4' [H5' H6]]]. case (H0 x). * case H6;auto. * auto. * intros x0 H; case (H0 z). -- tauto. -- auto. -- intros x1 H4; decompose [and] H6; subst a. destruct (cnf_plus H H4) as [x2 Hx2]; exists x2; auto. Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)