proposition: Lemma canon_lim3 i n alpha lambda : nf alpha -> nf lambda -> T1limit lambda -> canon (cons alpha n lambda) i = cons alpha n (canon lambda i).
proof: Proof. simpl (canon (cons alpha n lambda)). destruct alpha. - destruct n. + destruct lambda. * discriminate. * reflexivity. + destruct lambda. * discriminate. * reflexivity. - destruct n. * destruct lambda. -- discriminate. -- reflexivity. * destruct lambda. -- discriminate. -- reflexivity. Qed.
imports: hydras.Prelude(DecPreOrder)