proposition: Lemma has_bool_correct : forall am i, has_bool am i = true -> eval_prop am IsProp i <-> is_true (eval_prop am IsBool i).
proof: Proof. unfold has_bool, eval_prop,is_true. intros. unfold bool_of_ptrie in H. destruct (IntMap.get' i am). - destruct a ; simpl in H. congruence. rewrite i0. unfold is_true; reflexivity. - simpl. intuition congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause