proposition: Lemma list_gt_list_is_sound_true : forall p lg ls, list_gt_list p lg ls = Some true -> (forall s, In s ls -> exists g, In g lg /\ p g s = Some Greater_than).
proof: Proof. intros. assert (H1:=@list_gt_list_is_sound p lg ls). rewrite H in H1. assert (H1':= H1 s). apply H1'. 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)