proposition: Lemma literal_eq : forall l, literal_of_bool (is_positive_literal l) (form_of_literal l) = l.
proof: Proof. destruct l ; simpl ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause