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