proposition: Lemma canonS_phi0_succ_eqn i gamma: nf gamma -> canon (T1.phi0 (succ gamma)) (S i) = cons gamma i zero.
proof: Proof. intros; cbn. rewrite T1.pred_of_succ; case_eq (T1.succ gamma); trivial. - intro; destruct (succ_not_zero _ H0); auto 2. Qed.
imports: hydras.Prelude(DecPreOrder)