proposition: Lemma lforall_notin_solved_eqn_mem : forall n x l, lforall (notin_solved_eqn n) l -> beq_nat x n = false -> mem n (vars (subst_of_solved_eqns l x)) = false.
proof: Proof. induction l. simpl. mem. auto. simpl. destruct a. unfold notin_solved_eqn at 1. simpl. split_all. unfold extend. case_beq_nat x n0; tauto. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)