proposition: Lemma list_gt_list_is_sound_none: forall p lg ls, list_gt_list p lg ls = None -> (exists t1: term, In t1 ls /\ ((exists t2:term, In t2 lg /\ p t2 t1 = None) /\ (forall t2, In t2 lg -> p t2 t1 = Some Greater_than -> False))).
proof: Proof. intros. case_eq (list_gt_list p lg ls). intros. destruct b. rewrite H in H0. discriminate. rewrite H in H0. discriminate. intros. unfold list_gt_list in H0. assert (H1 := @list_forall_option_is_sound term (fun s : term => list_exists_option (fun g : term => match p g s with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) lg) ls). rewrite H0 in H1. destruct H1. destruct H1. assert (H3:= @list_exists_option_is_sound term (fun g : term => match p g x with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) lg). rewrite H2 in H3. destruct H3. exists x. split. trivial. split. destruct H3. exists x0. case_eq (p x0 x). intros. destruct c. rewrite H5 in H3. destruct H3. discriminate. rewrite H5 in H3. destruct H3. discriminate. rewrite H5 in H3. destruct H3. discriminate. rewrite H5 in H3. destruct H3. discriminate. intros. rewrite H5 in H3. destruct H3. split. assumption. trivial. intros. assert (H4' := H4 t2). rewrite H6 in H4'. apply H4'. trivial. 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)