proposition: Lemma mult_eval_is_sound_weak : forall p l1 l2, match mult_eval p l1 l2 with | Some Equivalent => False | Some Less_than => forall t1, In t1 l1 -> exists t2, In t2 l2 /\ p t2 t1 = Some Greater_than | Some Greater_than => forall t2, In t2 l2 -> exists t1, In t1 l1 /\ p t1 t2 = Some Greater_than | _ => True end.
proof: Proof. intros p l1 l2; unfold mult_eval. generalize (list_gt_list_is_sound p l1 l2); destruct (list_gt_list p l1 l2) as [[ | ] | ]; trivial. intros; generalize (list_gt_list_is_sound p l2 l1); destruct (list_gt_list p l2 l1) as [[ | ] | ]; 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)