proposition: Lemma cnf_eq alpha beta ol ol': sorted (cons alpha ol) -> sorted (cons beta ol') -> eval (cons alpha ol) = eval (cons beta ol') -> alpha = beta /\ eval ol = eval ol'.
proof: Proof. intros H H0 H1; generalize (cnf_head_eq H H0 H1). intro; subst beta; split;[trivial | ]. simpl in H1; now eapply plus_reg_r with (phi0 alpha). Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)