fact: Definition opp_literal (l1 l2: literal) : bool := match l1 , l2 with | POS f , NEG f' | NEG f , POS f' => id f =? id f' | _ , _ => false end.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause