proposition: Lemma world_finite: forall w: world, exists l: list adr, forall a:adr, In a l <-> lookup_fpm w a <> None.
proof: Proof. intro; destruct w as [f [li ?]]; simpl; exists (extractSome f li); split; intros. clear e; induction li; simpl in H; auto. destruct (f a0) eqn: ?. destruct (in_inv H). subst. rewrite Heqo. intro. inversion H0. apply IHli; auto. apply IHli; auto. destruct (in_dec nat_eq_dec a li). clear e. induction li; simpl in *; auto. destruct (f a0) eqn : ?. destruct i. subst. apply in_eq. apply in_cons. apply IHli; auto. destruct i. subst. exfalso; auto. apply IHli; auto. specialize (e a n). exfalso; auto. Qed.
imports: VST.msl.msl_direct CertiGraph.msl_ext.abs_addr Peano_dec