proposition: Lemma subterm_eq_sn : forall t, SNR t -> forall u, subterm_eq u t -> SNR u.
proof: Proof. intros t H. elim H. clear t H. intros t H IH u H0. apply SN_intro. intros u' H1. ded (red_subterm H1 H0). destruct H2 as [t']. destruct H2. eapply IH. apply H2. hyp. Qed.
imports: CoLoR(ATrs SN LogicUtil VecUtil VecOrd NatUtil RelUtil ARelation Union ACap ACalls) Coq(List Sumbool)