proposition: Lemma mem_in_1: forall t: term, forall A, mem eq t A -> In t A.
proof: Proof. intro t. induction A. intros. unfold mem in H. contradiction. unfold mem. unfold In. intro H. destruct H. left. rewrite H. trivial. right. assert (In 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)