proposition: Lemma wf_weaken: forall A (pt: ptrie A) p brb brb' lr, wf (Some (p, brb, brb', lr)) pt -> forall n n', (forall q, Key.testbit n q = true <-> n' = q) -> (n' < brb')%nat -> wf (Some (Key.mask p n, n, n', Key.zerobit p n)) pt.
proof: Proof. intros A t; induction t; intros. - constructor. - inv H; constructor; auto. + symmetry. rewrite ! (Key.zerobit_spec _ _ _ H0). f_equal. auto. + eapply Key.mask_spec'. eauto. + intros. eapply Key.mask_spec; eauto. + intros. rewrite <- Hprefix; try lia. eapply Key.mask_spec; eauto. - inv H; econstructor; trivial. + symmetry. rewrite ! (Key.zerobit_spec _ _ _ H0). f_equal. auto. + eapply Key.mask_spec'. eauto. + eapply lt_trans; eauto. + assumption. + assumption. + intros; eapply Key.mask_spec; eauto. + intros. rewrite <- Hprefix; try lia. eapply Key.mask_spec; eauto. + assumption. + assumption. Qed.
imports: Lia Cdcl.Coqlib