proposition: Lemma remove_equiv_eval_list_fully_evaluates : forall p l1 l2, (forall t1 t2, In t1 l1 -> In t2 l2 -> p t1 t2 <> None) -> remove_equiv_eval_list p l1 l2 <> None.
proof: Proof. intros p l1 l2 E; functional induction (remove_equiv_eval_list p l1 l2) as [ l1 | H1 l2 H2 H3 H4 H' | H1 l2 t1 l1 H2 H3 H4 H' l2' H IH | H1 l2 t1 l1 H2 H3 H4 H' H IH l1' l2' R | H1 l2 t1 l1 H2 H3 H4 H' H IH R | H1 l2 t1 l1 H2 H3 H4 H' H]. discriminate. discriminate. assert (K := remove_equiv_eval_is_sound p t1 H3); rewrite H in K; destruct K as [t2 [t2_in_l2 P2]]; apply IH; intros u1 u2 u1_in_l1 u2_in_l2'; apply E; trivial. right; trivial. rewrite (in_permut_in P2); right; trivial. discriminate. rewrite R in IH; apply IH; intros u1 u2 u1_in_l1 u2_in_l2; apply E; trivial; right; trivial. assert (K := remove_equiv_eval_fully_evaluates p t1 H3); rewrite H in K; intros _; apply K; trivial. intros t2 t2_in_l2; apply E; 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)