proposition: Lemma mem_vars_size_sub_ge : forall s x u, mem x (vars u) = true -> size (sub s u) >= size (s x).
proof: Proof. intros s x u. pattern u. apply term_ind with (Q := fun n (ts : terms n) => mem x (vars_vec ts) = true -> size_terms (Vmap (sub s) ts) >= size (s x)); clear u. intro. simpl. mem. intro. subst x0. lia. intros f v. rewrite vars_fun, sub_fun, size_fun. intros. ded (H H0). lia. simpl. mem. intros. discr. intros until v. simpl. mem. intros. destruct (orb_true_elim H1). ded (H e). lia. ded (H0 e). lia. Qed.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)