proposition: Lemma wf_nb_vars_lt : well_founded nb_vars_lt.
proof: Proof. unfold nb_vars_lt. apply wf_inverse_image with (B := nat). exact lt_wf. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)