proposition: Lemma lookup_fpm_join_sub: forall (w1 w2 : world) x, join_sub w1 w2 -> lookup_fpm w1 x <> None -> lookup_fpm w2 x <> None.
proof: Proof. intros. destruct H as [w3 ?]. destruct w1 as [f1 [l1 ?]]. destruct w2 as [f2 [l2 ?]]. destruct w3 as [f3 [l3 ?]]. hnf in H; simpl in *. specialize (H x). inversion H. exfalso; auto. auto. auto. Qed.
imports: VST.msl.msl_direct CertiGraph.msl_ext.abs_addr Peano_dec