proposition: Lemma mem_in_2: forall t: term, forall A, In t A -> mem eq t A.
proof: Proof. intro t. induction A. intros. unfold In in H. contradiction. unfold In. unfold mem. intro H. destruct H. left. rewrite H. trivial. right. assert (mem eq t A). apply IHA. assumption. assumption. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)