proposition: Lemma remove_equiv_is_sound_some : forall t l l', remove_equiv t l = Some l' -> {t' | equiv t t' /\ permut0 equiv l (t' :: l')}.
proof: Proof. intros t l; induction l as [ | a l]; intros l' R; simpl in R. discriminate. destruct (equiv_dec t a) as [t_eq_a | t_diff_a]. injection R; intro; subst l'; clear R; exists a; split; reflexivity || auto. destruct (remove_equiv t l) as [ l'' | ]. injection R; intro; subst l'; clear R. destruct (IHl l'' (eq_refl _)) as [t' [t_eq_t' P]]. exists t'; split; trivial. rewrite <- (@permut0_cons_inside _ _ equiv_equiv a a l (t' :: nil) l''); trivial. reflexivity. discriminate. 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)