fact: Definition ForallPair {A: Type} (P : A -> Prop) (x : A * A) := P (fst x) /\ P (snd x).
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause