proposition: Lemma wf_Some_Branch: forall {A: Type} {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 = mask p' m). + eapply testbit_spec; intros. generalize (mask_spec p' _ _ Hbrb); intros [HA HB]. destruct (lt_dec n0 n). * rewrite HA; eauto. * rewrite HB; try lia. eapply Hlength'. lia. + rewrite H. apply wf_weaken with (1:=H2); auto. - assert (p = mask p' m). + eapply testbit_spec; intros. generalize (mask_spec p' _ _ Hbrb); intros [HA HB]. destruct (lt_dec n0 n). * rewrite HA; eauto. * rewrite HB; try lia. eapply Hlength'. lia. + rewrite H. apply wf_weaken with (1:= H9); auto. Qed.
imports: List Bool ZArith Lia