proposition: Lemma mem_vars_size_sub_gt : forall s x u, mem x (vars u) = true -> u <> Var x -> size (sub s u) > size (s x).
proof: Proof. intros. destruct u. simpl in H. autorewrite with mem in H. subst n. cong. clear H0. rewrite sub_fun, size_fun. rewrite vars_fun in H. destruct (mem_vars_vec H). destruct H0. ded (Vin_elim H0). decomp H2. rewrite H3, Vmap_cast, size_terms_cast, Vmap_app, size_terms_app. simpl. ded (mem_vars_size_sub_ge s H1). lia. Qed.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)