proposition: Lemma lforall_notin_vars_solved_eqn_1 : forall n t0 t1 l' l, lforall (notin ((Var n, t0) :: l')) l -> lforall (notin_vars_solved_eqn t1) l -> lforall (notin_vars_solved_eqn (sub (single n t0) t1)) (map (solved_eqn_sub (single n t0)) l).
proof: Proof. induction l; simpl. auto. destruct a. unfold solved_eqn_sub at 1, notin_vars_solved_eqn at 1 3, notin_eqn. simpl. split_all. apply mem_vars_sub_single; hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)