proposition: Lemma updater_fst: forall (A B: Type) acc (f:A -> B) g (j: key) (m: ptrie A) , fst (updater f g acc j m) = update (fun x => g (f x)) j m.
proof: Proof. induction m; simpl; intros. - reflexivity. - destruct (eqb j k);auto. destruct (g (f v)); auto. - destruct (match_prefix j prefix brbit); auto. destruct (zerobit j brbit). destruct (updater f g acc j m1). simpl in *. congruence. destruct (updater f g acc j m2). simpl in *. congruence. Qed.
imports: List Bool ZArith Lia