proposition: Lemma in_elements': forall {A: Type} (m: ptrie A) k i v opt, wf opt m -> In (i, v) (elements' m k) -> get' i m = Some v \/ In (i, v) k.
proof: Proof. induction m; intros. - simpl in H0; right; auto. - simpl in H0; simpl; destruct H0; auto. inv H0. rewrite eqb_refl. left; reflexivity. - simpl in H0. inv H. { eapply IHm1 in H0. destruct H0. + left. simpl. case_eq (zerobit i brbit); intros; auto. generalize (get_not_same_lr H4 H0); congruence. + eapply IHm2 in H; eauto. destruct H; auto. left. simpl. case_eq (zerobit i brbit); intros; auto. generalize (get_not_same_lr H7 H0); congruence. + exact H4. } { eapply IHm1 in H0. destruct H0. + left. simpl. case_eq (zerobit i brbit); intros; auto. generalize (get_not_same_lr H4 H0); congruence. + eapply IHm2 in H; eauto. destruct H; auto. left. simpl. case_eq (zerobit i brbit); intros; auto. generalize (get_not_same_lr H7 H0); congruence. + exact H4. } Qed.
imports: List Bool ZArith Lia