proposition: Lemma wf_remove': forall A opt i (t: ptrie A), wf opt t -> wf opt (remove' i t).
proof: Proof. induction 1; intros. - constructor. - simpl; destruct (elt_eqb k i) eqn:EQ; constructor; auto. - simpl; destruct (elt_eqb k i); constructor; auto. - simpl. case_eq (Key.match_prefix i prefix brbit); intros. + destruct (Key.zerobit i brbit); eapply wf_branch; eauto. + econstructor; eauto. - simpl. case_eq (Key.match_prefix i prefix brbit); intros. + destruct (Key.zerobit i brbit); eapply wf_branch'; eauto. + econstructor; eauto. Qed.
imports: Lia Cdcl.Coqlib