proposition: Lemma wf_Some_Branch: forall A p m n lr p' m' (t1 t2: ptrie A), wf (Some (p, m, n, lr)) (Branch p' m' t1 t2) -> wf (Some (p, m, n, lr)) t1 /\ wf (Some (p, m, n, lr)) t2.
proof: Proof. intros; inv H; split. - assert (p = Key.mask p' m). + eapply Key.testbit_spec; intros. generalize (Key.mask_spec p' _ _ Hbrb); intros [HA HB]. destruct (lt_dec n0 n). * rewrite HA; auto. * rewrite HB; try lia. eapply Hlength'. lia. + rewrite H. apply (wf_weaken H2 Hbrb Hincr). - assert (p = Key.mask p' m). + eapply Key.testbit_spec; intros. generalize (Key.mask_spec p' _ _ Hbrb); intros [HA HB]. destruct (lt_dec n0 n). * rewrite HA; auto. * rewrite HB; try lia. eapply Hlength'. lia. + rewrite H. apply (wf_weaken H9 Hbrb Hincr). Qed.
imports: Lia Cdcl.Coqlib