proposition: Lemma canon0_cons_succ_eqn2 n gamma : nf gamma -> canon (cons (T1.succ gamma) (S n) zero) 0= cons (T1.succ gamma) n zero.
proof: Proof. intros; cbn; rewrite T1.pred_of_succ; case_eq (T1.succ gamma); trivial. Qed.
imports: hydras.Prelude(DecPreOrder)