proposition: Lemma cnf_head_eq alpha beta ol ol': sorted (cons alpha ol) -> sorted (cons beta ol') -> eval (cons alpha ol) = eval (cons beta ol') -> alpha = beta.
proof: Proof. intros H H0 H1; tricho alpha beta H2; [ | trivial | ]. - generalize (sorted_lt_lt H H2) ; intro H3. case (@lt_irrefl (eval (cons alpha ol))). apply lt_le_trans with (phi0 beta); [trivial | ]. + rewrite H1; simpl ; apply le_plus_l. - generalize (sorted_lt_lt H0 H2); intro H3. case (@lt_irrefl (eval (cons beta ol'))). apply lt_le_trans with (phi0 alpha); [trivial | ]. + rewrite <- H1; simpl; apply le_plus_l. Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)