proposition: Lemma has_boolb_mono : forall b t1 t2, OBool.order t1 t2 -> OBool.has_boolb b t1 = true -> OBool.has_boolb b t2 = true.
proof: Proof. unfold OBool.has_boolb. destruct t1, t2 ; simpl; try tauto. intros; subst; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause