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