proposition: Lemma o_term_list_is_o_term_list : forall l1 l2, o_term_list l1 l2 = ((fix o_term_list (l : list term) : list term -> bool := fun l' : list term => match l with | nil => match l' with | nil => true | _ :: _ => false end | h :: tl => match l' with | nil => true | h' :: tl' => if T1.eq_bool h h' then o_term_list tl tl' else o_bool h h' end end)) l1 l2.
proof: Proof. induction l1; induction l2; trivial. Qed.
imports: Coq(Relations List) CoLoR(list_sort term_spec)