proposition: Lemma equiv_dec : forall t1 t2, {equiv t1 t2}+{~equiv t1 t2}.
proof: Proof. intros t1 t2; generalize (equiv_bool_ok t1 t2); case (equiv_bool t1 t2). left; assumption. right; assumption. Defined.
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)