proposition: Theorem cnf_exists_unique (alpha:Ord) : exists! l: cnf_t, is_cnf_of alpha l.
proof: Proof. destruct (cnf_exists alpha) as [l Hl]; exists l; split; auto. now apply cnf_unicity. Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)