proposition: Lemma remove_equiv_eval_fully_evaluates : forall p t l, (forall t', In t' l -> p t t' <> None) -> remove_equiv_eval p t l <> @Not_finished _.
proof: Proof. intros p t l E; functional induction (remove_equiv_eval p t l) as [ | H1 a l t' H | H1 a l t' H IH l' H' | H1 a l t' H IH H' | H1 a l t' H IH H' | H1 a l t' H]. discriminate. discriminate. discriminate. discriminate. rewrite H' in IH; apply IH; intros; apply E; right; trivial. assert (H' := E _ (or_introl _ (eq_refl _)) H); contradiction. 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)