fact: Fixpoint cnf_checker (f : cnf) (l : list Witness) {struct f}: bool := match f with | nil => true | e::f => match l with | nil => false | c::l => match checker e c with | true => cnf_checker f l | _ => false end end end.
imports: List Refl Bool Relation_Definitions Setoid