proposition: Lemma gmem' : forall {A: Type} (i:key) (t: ptrie A), mem' i t = is_Some (get' i t).
proof: Proof. induction t ; simpl ; auto. destruct (eqb i k) ; reflexivity. destruct (zerobit i brbit) ; auto. Qed.
imports: List Bool ZArith Lia