proposition: Lemma not_empty_get': forall {A: Type} {pt: ptrie A} {opt}, wf opt pt -> pt <> Empty -> exists k v, get' k pt = Some v.
proof: Proof. induction pt; intros. - elim H0; reflexivity. - exists k, v; simpl; rewrite eqb_refl; congruence. - assert (HA: exists k1 v1, get' k1 pt1 = Some v1) by (inv H; eapply IHpt1; eauto). assert (HB: exists k2 v2, get' k2 pt2 = Some v2) by (inv H; eapply IHpt2; eauto). simpl. destruct HA as [k1 [v1 HA]]. exists k1, v1; rewrite HA. case_eq (zerobit k1 brbit); intros; auto. assert (get' k1 pt1 = None) by (inv H; eapply get_not_same_lr; eauto). congruence. Qed.
imports: List Bool ZArith Lia