proposition: Lemma wf_term_var : forall s x u, s x = sub s u -> mem x (vars u) = true -> u = Var x.
proof: Proof. intros. ded (mem_vars_size_sub_gt s H0). rewrite H in H1. case (eq_term_dec u (Var x)). auto. intro. ded (H1 n). lia. Qed.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)