proposition: Lemma list_gt_list_is_complete_true: forall p lg ls, ( forall s, In s ls -> exists g, In g lg /\ p g s = Some Greater_than) -> list_gt_list p lg ls = Some true.
proof: Proof. induction ls. intros. compute. trivial. intros. unfold list_gt_list. apply list_forall_option_is_complete_true. intros. apply list_exists_option_is_complete_true. assert (H1:= H a0). assert (exists g : term, In g lg /\ p g a0 = Some Greater_than). apply H1; trivial. destruct H2. destruct H2. exists x. split; trivial. rewrite H3. 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)