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