proposition: Lemma lforall_notin_r : forall x t l' l, lforall (notin ((t, Var x) :: l')) l -> lforall (notin (map (eqn_sub (single x t)) l')) (map (solved_eqn_sub (single x t)) l).
proof: Proof. induction l; simpl. auto. destruct a. simpl. unfold notin_eqn. simpl. mem. split_all. unfold notin. simpl. unfold notin in H2. simpl in H2. apply lforall_notin_eqn; hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)