proposition: Lemma remove_equiv_eval_is_sound : forall p t l, match remove_equiv_eval p t l with | Found l' => exists t', p t t' = Some true /\ list_permut.permut0 (@eq term) l (t' :: l') | Not_found => forall t', In t' l -> p t t' = Some false | Not_finished => exists t', In t' l /\ p t t' = None end.
proof: Proof. intros p t l; 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]. simpl; intros; contradiction. exists a; split; auto. apply list_permut.permut_refl; intro; trivial. rewrite H' in IH; destruct IH as [t' [H'' P]]; exists t'; split; trivial. apply (Pcons (R := @eq term) a a (l := l) (t' :: nil) l'); trivial. rewrite H' in IH; intros t' [a_eq_t' | t'_in_l]; [subst | apply IH]; trivial. rewrite H' in IH; destruct IH as [t' [t'_in_l ptt'_eq_none]]; exists t'; split; trivial; right; trivial. exists a; split; trivial; left; trivial. 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)