proposition: Lemma lexico_eval_equation : forall p s1 s2 l1 l2, lexico_eval p s1 s2 l1 l2 = match l1, l2 with | nil, nil => Some Equivalent | nil, (_ :: _) => Some Less_than | (_ :: _), nil => Some Greater_than | (t1 :: l1'), (t2 :: l2') => match p t1 t2 with | Some Equivalent => lexico_eval p s1 s2 l1' l2' | Some Greater_than => match term_gt_list p s1 l2 with | Some true => Some Greater_than | Some false => Some Uncomparable | None => None end | Some Less_than => match term_gt_list p s2 l1 with | Some true => Some Less_than | Some false => Some Uncomparable | None => None end | Some Uncomparable => Some Uncomparable | None => None end end.
proof: Proof. intros p s1 s2 [ | t1 l1] [ | t2 l2]; apply eq_refl. 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)