proposition: Lemma gmap': forall (A B: Type) (f: key -> A -> B) (i: key) (m: ptrie A), get' i (map' f m) = option_map (f i) (get' i m).
proof: Proof. induction m; intros. - reflexivity. - simpl. repeat rewrite eqb_is_dec;destruct (eq i k); simpl; auto; congruence. - simpl. destruct (zerobit i brbit); simpl; auto. Qed.
imports: List Bool ZArith Lia