fact: Definition disjointed {A: Type} {JA: Join A} (P Q: pred A):= forall h1 h2 h3 h12 h23, join h1 h2 h12 -> join h2 h3 h23 -> P h12 -> Q h23 -> identity h2 /\ joins h1 h3.
imports: CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext VST.msl.msl_direct CertiGraph.msl_ext.sepalg