proposition: Lemma remove_equiv_is_sound_none : forall t l, remove_equiv t l = None -> forall t', mem equiv t' l -> ~ (equiv t t').
proof: Proof. intros t l; functional induction (remove_equiv t l) as [ | H1 a l t' t_eq_a _ | H1 a l t' t_diff_a _ IH H | H1 a l t' t_diff_a _ IH l' H ]. simpl; intros; contradiction. intros; discriminate. intros _; rewrite H in IH; intros t' [a_eq_t' | t'_mem_l]. intro t_eq_t'; apply t_diff_a. transitivity t'; trivial. apply IH; trivial. intros; 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)