proposition: Lemma wf_update: forall A f opt i (t: ptrie A), wf opt t -> wf opt (update f i t).
proof: Proof. induction 1; intros. - constructor. - simpl. destruct (f v). + destruct (eqb i k) eqn:EQ. * apply eqb_spec in EQ. subst. constructor; auto. * constructor; auto. + destruct (eqb i k) eqn:EQ. * apply eqb_spec in EQ. subst. constructor; auto. * constructor; auto. - simpl. destruct (f v). + destruct (eqb i k) eqn:EQ. * apply eqb_spec in EQ. subst. constructor; auto. * constructor; auto. + destruct (eqb i k) eqn:EQ. * apply eqb_spec in EQ. subst. constructor; auto. * constructor; auto. - simpl. case_eq (match_prefix i prefix brbit); intros. + destruct (zerobit i brbit); eapply wf_branch; eauto. + econstructor; eauto. - simpl. case_eq (match_prefix i prefix brbit); intros. + destruct (zerobit i brbit); eapply wf_branch'; eauto. + econstructor; eauto. Qed.
imports: List Bool ZArith Lia