proposition: Lemma step_N b : forall r, noSubterm_R r b -> noSubterm_TR (N r) b with step_rcons1 b : forall t r, noSubterm_T t b -> noSubterm_RT (rcons t r) b with step_rcons2 b : forall t r, noSubterm_R r b -> noLargeSubterm_R (rcons t r) b with step_aux1 b : forall r, noSubterm_RT r b -> noLargeSubterm_T (N r) b with step_aux2 b : forall t r, noSubterm_TR t b -> noLargeSubterm_R (rcons t r) b with step_aux3 b : forall t r, noSubterm_RT r b -> noSubterm_RT (rcons t r) b.
proof: Proof. * destruct b; intros r H. - exact I. - split. + apply step_aux1. apply H. + refine (I, _). change (noSubterm_TR (N r) b). apply step_N. apply H. * destruct b; intros t r H. - exact I. - apply step_aux2. apply H. * destruct b; intros ? r H. - split. + intros H'; noconf H'. + exact I. - split. + intros H'; noconf H'. apply H; reflexivity. + split. -- refine (I, _). change (noSubterm_RT (rcons t0 r) t). apply step_aux3. apply H. -- apply step_rcons2. apply H. * destruct b; intros r H. - split. + intros H'; noconf H'. + exact I. - split. + intros H'; noconf H'. apply H; reflexivity. + refine (I, _). change (noSubterm_TR (N r) x). apply step_N. apply H. * destruct b; intros ? r H. - split. + intros H'; noconf H'. + exact I. - split. + intros H'; noconf H'. apply H; reflexivity. + split. -- refine (I, _). change (noSubterm_RT (rcons t0 r) t). apply step_rcons1. apply H. -- apply step_aux2. apply H. * destruct b; intros t r H. - exact I. - apply step_rcons2. apply H. Qed.
imports: Equations(Equations) Below