proposition: Lemma bempty: forall (A: Type) (m: ptrie A) opt, wf opt m -> (forall x, get' x m = None) <-> m = Empty.
proof: Proof. induction m; intros. - split; intros; simpl; auto. - split; try discriminate; intros. generalize (H0 k); simpl; rewrite elt_eqb_refl; congruence. - split; intros; try discriminate. inv H. + elim Hl. eapply IHm1; eauto. simpl in H0. intros. case_eq (Key.zerobit x brbit); intros. * generalize (H0 x); rewrite H; auto. * eapply get_not_same_lr; eauto. + elim Hl. eapply IHm1; eauto. simpl in H0. intros. case_eq (Key.zerobit x brbit); intros. * generalize (H0 x); rewrite H; auto. * eapply get_not_same_lr; eauto. Qed.
imports: Lia Cdcl.Coqlib