proposition: Lemma lt_card_vars_eqns_subs_l : forall x v l, mem x (vars v) = false -> cardinal (vars_eqns (map (eqn_sub (single x v)) l)) < cardinal (vars_eqns ((Var x, v) :: l)).
proof: Proof. intros. simpl. unfold vars_eqn. simpl. apply subset_cardinal_lt with x. trans (if mem x (vars_eqns l) then union (vars v) (remove x (vars_eqns l)) else vars_eqns l). apply subset_equal. apply vars_eqns_subs. case_eq (mem x (vars_eqns l)); intros H0 z; set_iff; tauto. set_iff; tauto. intro H0. rewrite (In_m (refl_equal x) (vars_eqns_subs x v l)) in H0. revert H0. case_eq (mem x (vars_eqns l)); intro e; set_iff. ded (mem_4 _ _ H). tauto. ded (mem_4 _ _ e). tauto. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)