proposition: Lemma get_not_same_lr: forall A (t: ptrie A) p brb brb' lr k, wf (Some (p, brb, brb', lr)) t -> Key.zerobit k brb = negb lr -> get' k t = None.
proof: Proof. intros A t; induction t; intros. - reflexivity. - inv H. simpl. rewrite elt_eqb_is_dec ; destruct (elt_eq k0 k); auto. subst k0. destruct (Key.zerobit k brb); simpl in H0; congruence. - inv H. simpl. case_eq (Key.zerobit k brbit); intros. + eapply IHt1. * eapply wf_weaken; trivial. exact H3. auto. * eauto. + eapply IHt2. * eapply wf_weaken; trivial. exact H10. auto. * eauto. Qed.
imports: Lia Cdcl.Coqlib