proposition: Lemma lforall_notin_vars_solved_eqn_mem : forall x u l, lforall (notin_vars_solved_eqn u) l -> mem x (dom l) = true -> mem x (vars u) = false.
proof: Proof. induction l. simpl. mem. intros. discr. destruct a. simpl. mem. unfold notin_vars_solved_eqn at 1. simpl. split_all. destruct (orb_true_elim H0). rewrite beq_nat_ok in e. subst n. hyp. auto. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)