fact: Definition xror_clause_cnf t f := List.fold_left (fun '(acc,tg) e => match ror_clause t e with | inl cl => (cl :: acc,tg) | inr l => (acc,merge tg l) end) f (nil, null).
imports: List Refl Bool Relation_Definitions Setoid