proposition: Lemma join_sub_mapsto: forall w1 w2 x y, join_sub w1 w2 -> (mapsto x y * TT)%pred w1 -> (mapsto x y * TT)%pred w2.
proof: Proof. intros. destruct_sepcon H0 h. destruct H as [w3 ?]. try_join h2 w3 m. exists h1, m. split; auto. Qed.
imports: VST.msl.msl_direct FunctionalExtensionality CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.overlapping_direct CertiGraph.heap_model_direct.SeparationAlgebra Peano_dec