proposition: Lemma Canon_plus_first_step_lim: forall i alpha beta, E0limit alpha -> Canon_plus (S i) alpha beta -> beta = Canon alpha (S i) \/ Canon_plus (S i) (Canon alpha (S i)) beta.
proof: Proof. destruct alpha, beta. unfold Canon_plus, const_path; simpl. intros H H0; destruct (const_pathS_first_step H0). - left; unfold Canon; f_equal; f_equal; simpl; subst cnf0. f_equal; apply nf_proof_unicity. - right; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)