proposition: Lemma in_mem : forall s l, In s l -> mem equiv s l.
proof: Proof. intro s. induction l. intro H. unfold In in H. auto. intro H. unfold In in H. destruct H. rewrite H. simpl. left. reflexivity. simpl. right. auto. 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)