proposition: Lemma get_not_same_prefix: forall A (t: ptrie A) p brb brb' lr, wf (Some (p, brb, brb', lr)) t -> forall k n, (n < brb')%nat -> Key.testbit p n <> Key.testbit k n -> get' k t = None.
proof: Proof. intros A t. induction t; intros. - reflexivity. - inv H; simpl. destruct (elt_eqb k0 k)eqn:EQ; auto. rewrite K.eqb_spec in EQ. subst k0. elim H1. apply Hprefix; auto. - inv H; simpl. case_eq (Key.zerobit k brbit); intros; auto. + eapply IHt1 with (n := n); eauto. lia. + eapply IHt2 with (n := n); eauto. lia. Qed.
imports: Lia Cdcl.Coqlib