proposition: Lemma Lt_eqns_subs_r : forall x v l, mem x (vars v) = false -> Lt (map (eqn_sub (single x v)) l) ((v, Var x) :: l).
proof: Proof. intros. unfold Lt, lt, transp. apply lex_intro. left. unfold nb_vars_lt. apply lt_card_vars_eqns_subs_r. hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)