proposition: Lemma cnf_unicity l alpha: is_cnf_of alpha l -> forall l', is_cnf_of alpha l' -> l = l'.
proof: Proof. revert alpha; induction l. - destruct 1 as [H H0]. simpl in H0; subst alpha; destruct l'. + auto. + destruct 1 as [H0 H1]; simpl in H1; case (@lt_irrefl zero). pattern zero at 2;rewrite H1. apply lt_le_trans with (phi0 o);auto with schutte. apply phi0_positive. apply le_plus_l;auto. - destruct l' as [ | o l']. + intro; case H;case H0;intros H1 H2 H3 H4. simpl in H2, H4 ; rewrite H2 in H4. assert (ordinal a) by split. case (@lt_irrefl zero). pattern zero at 2; rewrite H4. apply lt_le_trans with (phi0 a);auto. * apply phi0_positive. * apply le_plus_l;auto. + intro; case H; case H0;intros H1 H2 H3 H4; rewrite H4 in H2. case (cnf_eq H3 H1 H2). intros; subst o; replace l' with l;auto. * apply IHl with (eval l). split;auto. inversion H3; auto with schutte. rewrite H6;split;auto with schutte. inversion H1; auto with schutte. Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)