fact: Definition o_term_list := (fix o_term_list (l1:list term) : list term -> bool := fun l2 => match l1, l2 with | nil, nil => true | _ :: _, nil => true | nil, _ :: _ => false | h1 :: tl1, h2 :: tl2 => if T1.eq_bool h1 h2 then o_term_list tl1 tl2 else o_bool h1 h2 end).
imports: Coq(Relations List) CoLoR(list_sort term_spec)