proposition: Lemma cnf_plus1 (ol : cnf_t) : sorted ol -> forall alpha, exists ol', is_cnf_of (phi0 alpha + eval ol) ol'.
proof: Proof. induction ol. - inversion_clear 1 . intros alpha; simpl; exists (cons alpha nil). split. + constructor. + split ; simpl. - intros H alpha; simpl; tricho alpha a H1. + exists (cons a ol); split. * auto. * rewrite plus_assoc, phi0_alpha_phi0_beta; [simpl|]; auto. + subst a; exists (cons alpha (cons alpha ol)); split. * constructor; eauto with schutte. * simpl; auto. + exists (cons alpha (cons a ol)); split. * constructor;auto with schutte. * now simpl. Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)