proposition: Lemma ok_clause_test' p cl : ok_clause p cl = false -> exists y, In y cl /\ p y = None.
proof: Proof. apply (ok_clause_elim (fun e xs call => call = false -> exists y, In y xs /\ e y = None) (fun _ _ e xs call => call = false -> exists y, In y xs /\ e y = None)). all:try solve [cbn; try discriminate; firstorder eauto]. Qed.
imports: List ssreflect Equations.Prop.Equations