proposition: Lemma sub_eq' : forall s1 s2 (t : term), (forall x, mem x (vars t) = true -> s1 x = s2 x) -> sub s1 t = sub s2 t.
proof: Proof. intros. apply sub_eq. intro. rewrite in_vars_mem. auto. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)