proposition: Lemma o_bool_ok : forall t1 t2, match o_bool t1 t2 with true => o t1 t2 | false => ~o t1 t2 end.
proof: Proof. intros t1 t2; unfold o; case (o_bool t1 t2). reflexivity. discriminate. Defined.
imports: Coq(Relations List) CoLoR(list_sort term_spec)