proposition: Lemma canon_SSn_zero (i:nat) : forall alpha n , nf alpha -> canon (cons alpha (S n) zero) i = cons alpha n (canon (cons alpha 0 zero) i).
proof: Proof. intros; destruct (@zero_limit_succ_dec alpha); trivial. - destruct s. + destruct n; subst alpha; reflexivity. + rewrite canon_lim2 ; auto. rewrite canon_lim1; auto. - destruct s as [beta [Hdeta e]]; subst alpha. destruct i. rewrite canon0_cons_succ_eqn2, canon0_phi0_succ_eqn; auto. rewrite canonS_cons_succ_eqn2 , canonS_phi0_succ_eqn; auto. Qed.
imports: hydras.Prelude(DecPreOrder)