proposition: Lemma sub_sn : forall l x s, In x (vars l) -> SNR (sub s l) -> SNR (s x).
proof: Proof. intros. change (SNR (sub s (Var x))). eapply subterm_eq_sn. apply H0. apply subterm_eq_sub. apply in_vars_subterm_eq. hyp. Qed.
imports: CoLoR(ATrs SN LogicUtil VecUtil VecOrd NatUtil RelUtil ARelation Union ACap ACalls) Coq(List Sumbool)