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