proposition: Lemma has_bool_hold_eval_atom : forall k i, has_bool i = true -> eval_atom IsProp i <-> hold k (eval_atom k i).
proof: Proof. destruct k ; simpl; intros. tauto. apply has_bool_correct ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause