proposition: Lemma step_cons n x m b a : noSubterm n x m b -> noLargeSubterm (S n) (cons a x) m b.
proof: Proof. induction b; intros H. - split. + exact I. + constructor. - split. + pose proof (fst H). unfold cond_neq in H0. destruct (nat_dec n n0). * subst n. unfold cond_neq. destruct (nat_dec (S n0) (S n0)). -- rewrite <- DecidableEqDep_nat.eq_rect_eq in H0 |- *. intros H'; inversion H'. apply DecidableEqDep_nat.inj_pairT2 in H3. apply H0. apply H3. -- exact I. * unfold cond_neq. destruct (nat_dec (S n) (S n0)). -- inversion e. elim n1. apply H2. -- exact I. + apply (IHb (snd H)). Qed.
imports: Equations(Equations) Below Eqdep_dec