proposition: Lemma exists_exists_not : forall l2 a1 l1 n rpo_infos, (exists x, (In x l2) /\ (forall g : term, ~ In g (a1 :: l1) \/ rpo_eval rpo_infos n g x <> Some Greater_than)) -> (exists x, (In x l2) /\ ~ (exists g : term, In g (a1 :: l1) /\ rpo_eval rpo_infos n g x = Some Greater_than)).
proof: Proof. firstorder. 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)