proposition: Lemma find_is_sound : forall (I: term -> term -> Prop) l (l_sound: forall t t', In (t,t') l -> I t t') t1 t2, mem_bool eq_tt_bool (t1,t2) l = true -> I t1 t2.
proof: Proof. intros I l l_sound t1 t2 H; apply l_sound. apply (mem_impl_in (@eq (term*term))). intros; assumption. generalize (mem_bool_ok _ _ eq_tt_bool_ok (t1,t2) l); rewrite H; intros; 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)