proposition: Lemma disj_derives_d {A: Type} {JA: Join A} {PA: Perm_alg A}: forall P P' Q Q', P |-- P' -> Q |-- Q' -> disjointed P' Q' -> disjointed P Q.
proof: Proof. unfold derives, disjointed. intros. apply H1 with h12 h23; auto. Qed.
imports: CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext VST.msl.msl_direct CertiGraph.msl_ext.sepalg