proposition: Lemma elements_correct': forall (A: Type) (m: ptrie A) (i: elt) (v: A) k, get' i m = Some v -> In (i, v) (elements' m k).
proof: Proof. induction m; intros. - inv H. - simpl in H. repeat rewrite elt_eqb_is_dec in *;destruct (elt_eq i k); inv H. simpl. eapply in_eq. - simpl in H. case_eq (Key.zerobit i brbit); intros; rewrite H0 in H. + eapply IHm1; eauto. + simpl. eapply IHm2 in H. eapply elements_incl'; eauto. Qed.
imports: Lia Cdcl.Coqlib