proposition: Lemma dom_subst_of_solved_eqns : forall x l, mem x (dom l) = false -> subst_of_solved_eqns l x = Var x.
proof: Proof. induction l; simpl. mem. refl. destruct a. mem. intro. destruct (orb_false_elim H). unfold extend. rewrite (beq_com beq_nat_ok) in H0. rewrite H0. auto. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)