proposition: Lemma cnf_plus2 : forall ol, sorted ol -> forall ol', sorted ol' -> exists ol'', is_cnf_of (eval ol + eval ol') ol''.
proof: Proof. induction ol. - simpl; intros; rewrite zero_plus_alpha;auto. exists ol';split;auto. - intros; simpl; assert (sorted ol). { inversion H;auto with schutte. } destruct (IHol H1 _ H0) as [x [H3 H4]]. destruct (@cnf_plus1 _ H3 a) as [x0 H5]. exists x0; rewrite <- H4 in H5; now rewrite <- plus_assoc. Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)