proposition: Lemma list_gt_list_is_complete_none_1: forall p lg ls, list_gt_list p lg ls <> Some true -> list_gt_list p lg ls <> Some false -> list_gt_list p lg ls = None.
proof: Proof. intros. case_eq (list_gt_list p lg ls). intros. destruct b. contradict H. trivial. contradict H0. trivial. intros. 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)