proposition: Lemma Canon_plus_first_step: forall i alpha beta, Canon_plus (S i) (E0_succ alpha) beta -> alpha = beta \/ Canon_plus (S i) alpha beta.
proof: Proof. destruct alpha, beta. unfold Canon_plus, const_path; simpl ;intros H. destruct (const_pathS_first_step H). - rewrite canon_succ in e; auto. subst cnf0; assert (cnf_ok0 =cnf_ok). apply nf_proof_unicity. subst cnf_ok0; left;auto. - rewrite canon_succ in c;[ right;auto | auto]. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)