proposition: Lemma is_positive_literal_of_bool : forall b f, is_positive_literal (literal_of_bool b f) = b.
proof: Proof. unfold literal_of_bool. destruct b ; reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause