proposition: Lemma disj_data_at: forall sh t1 t2 p1 p2, sepalg.nonunit sh -> ~ pointer_range_overlap p1 (sizeof t1) p2 (sizeof t2) -> disjointed (EX v: reptype t1, data_at sh t1 v p1) (EX v: reptype t2, data_at sh t2 v p2).
proof: Proof. intros. eapply disj_derives; [| | apply disj_memory_block]. + apply exp_left; intro v. apply data_at_memory_block. + apply exp_left; intro v. apply data_at_memory_block. + auto. Qed.
imports: VST.floyd.base VST.floyd.client_lemmas VST.floyd.assert_lemmas VST.floyd.type_induction VST.floyd.nested_pred_lemmas VST.floyd.nested_field_lemmas VST.floyd.reptype_lemmas VST.floyd.field_at CertiGraph.veric_ext.seplog CertiGraph.veric_ext.SeparationLogic CertiGraph.floyd_ext.MapstoSL