proposition: Lemma T1limit_canonS_not_zero i lambda: nf lambda -> T1limit lambda -> canon lambda (S i) <> zero.
proof: Proof. destruct lambda as [ | alpha1 n alpha2]. - discriminate. - intros; simpl; destruct alpha1. + destruct n. * destruct alpha2 ; discriminate. * destruct alpha2; discriminate. + destruct n. * destruct alpha2. { destruct (T1.pred (cons alpha1_1 n0 alpha1_2)); discriminate. } discriminate. * destruct alpha2. destruct (T1.pred (cons alpha1_1 n0 alpha1_2)); discriminate. discriminate. Qed.
imports: hydras.Prelude(DecPreOrder)