proposition: Lemma nf_canon i alpha: nf alpha -> nf (canon alpha i).
proof: Proof. intros Hnf; destruct (T1_eq_dec alpha zero). - subst; constructor. - destruct i. destruct (canon0_LT Hnf); auto. destruct (canonS_LT i Hnf); auto. Qed.
imports: hydras.Prelude(DecPreOrder)