proposition: Lemma lforall_notin_vars_solved_eqn_dom : forall x u l, lforall (notin_vars_solved_eqn u) l -> mem x (vars u) = true -> mem x (dom l) = false.
proof: Proof. induction l; simpl. mem. refl. destruct a. unfold notin_vars_solved_eqn at 1. simpl. mem. split_all. case_beq_nat n x; simpl. rewrite H in H0. discr. apply IHl; hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)