proposition: Lemma remove_branch_not_empty: forall {A} [m: ptrie A] [prefix brbit m1 m2 o], wf o m -> m = Branch prefix brbit m1 m2 -> forall k, remove' k m <> Empty.
proof: Proof. induction m; intros; try congruence. eapply eq_sym in H0. inv H0. simpl. case_eq (match_prefix k prefix brbit); intros; try congruence. case_eq (zerobit k brbit); intros. - destruct m1. + inv H; congruence. + simpl. destruct_eq k0 k; simpl; try congruence. * inv H; congruence. * destruct m2; congruence. + assert (Ho: exists o1, wf o1 (Branch prefix0 brbit0 m1_1 m1_2)) by (inv H; eauto). destruct Ho as [o1 Ho1]. generalize (IHm1 _ _ _ _ _ Ho1 eq_refl k). intros HA. destruct (remove' k (Branch prefix0 brbit0 m1_1 m1_2)); destruct m2; simpl; inv H; try congruence. - destruct m2. + inv H; congruence. + simpl. destruct_eq k0 k; simpl; try congruence. * destruct m1; inv H; simpl; congruence. * destruct m1; inv H; simpl; congruence. + assert (Ho: exists o2, wf o2 (Branch prefix0 brbit0 m2_1 m2_2)) by (inv H; eauto). destruct Ho as [o2 Ho2]. generalize (IHm2 _ _ _ _ _ Ho2 eq_refl k). intros HA. destruct (remove' k (Branch prefix0 brbit0 m2_1 m2_2)); destruct m1; simpl; inv H; try congruence. Qed.
imports: List Bool ZArith Lia