proposition: Lemma gmap1': forall (A B: Type) (f: A -> B) (i: elt) (m: ptrie A), get' i (map1' f m) = option_map f (get' i m).
proof: Proof. induction m; intros. - reflexivity. - simpl. repeat rewrite elt_eqb_is_dec;destruct (elt_eq i k); simpl; auto; congruence. - simpl. destruct (Key.zerobit i brbit); simpl; auto. Qed.
imports: Lia Cdcl.Coqlib