proposition: Lemma term_gt_list_is_sound : forall p s l, match term_gt_list p s l with | Some true => forall t, In t l -> p s t = Some Greater_than | _ => True end.
proof: Proof. intros p s l; induction l as [ | t l]; simpl. intros; contradiction. replace (term_gt_list p s (t :: l)) with (match p s t with | Some Greater_than => term_gt_list p s l | Some _ => match term_gt_list p s l with Some _ => Some false | None => None end | None => None end). case_eq (p s t); [intros [ | | | ] H | trivial]. destruct (term_gt_list p s l) as [ [ | ] | ]; trivial. destruct (term_gt_list p s l) as [ [ | ] | ]; trivial. destruct (term_gt_list p s l) as [ [ | ] | ]; trivial. intros u [u_eq_t | u_in_l]; [subst | apply IHl]; assumption. destruct (term_gt_list p s l) as [ [ | ] | ]; trivial. unfold term_gt_list; simpl. destruct (p s t) 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)