fact: Fixpoint or_clause (cl1 cl2 : clause) : option clause := match cl1 with | nil => Some cl2 | t::cl => match add_term t cl2 with | None => None | Some cl' => or_clause cl cl' end end.
imports: List Refl Bool Relation_Definitions Setoid