proposition: Lemma canon_tail : forall alpha n beta i, nf (cons alpha n beta) -> beta <> 0 -> canon (cons alpha n beta) i = cons alpha n (canon beta i).
proof: Proof. destruct alpha as [| alpha1 n alpha2]. - destruct 2; auto. eapply nf_of_finite; eauto. - intros; simpl; destruct n0, beta; auto. + destruct H0; auto. + destruct H0; auto. Qed.
imports: hydras.Prelude(DecPreOrder)