proposition: Lemma canon_succ i alpha : nf alpha -> canon (succ alpha) i = alpha.
proof: Proof. revert i; induction alpha. - reflexivity. - destruct alpha1. + intros; replace alpha2 with zero. * reflexivity. * T1_inversion H; auto. + intros; simpl; destruct n. * destruct alpha2. { reflexivity. } { simpl;destruct alpha2_1. - f_equal; apply nf_inv2 in H. T1_inversion H; now subst. - f_equal. rewrite <- IHalpha2 with i; f_equal. eapply nf_inv2, H. } * case_eq (T1.succ alpha2). { intros; now destruct (@T1.succ_not_zero alpha2). } { intros; f_equal ; rewrite <- IHalpha2 with i. - now rewrite <- H0. - eapply nf_inv2, H. } Qed.
imports: hydras.Prelude(DecPreOrder)