proposition: Lemma equiv_eval_list_fully_evaluates : forall p l1 l2, (forall t1 t2, In t1 l1 -> In t2 l2 -> p t1 t2 <> None) -> equiv_eval_list p l1 l2 <> None.
proof: Proof. intros p l1 l2 E; functional induction (equiv_eval_list p l1 l2) as [ | H1 H2 t1 l1 H3 t2 l2 H4 H IH | H1 H2 t1 l1 H3 t2 l2 H4 H | H1 H2 t1 l1 H3 t2 l2 H4 H | l1 l2 H1 H2 H3 H4 H]. discriminate. apply IH; intros u1 u2 u1_in_l1 u2_in_l2; apply E; right; trivial. discriminate. assert (E' := E t1 t2); rewrite H in E'; apply E'; left; trivial. discriminate. 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)