proposition: Lemma disj_emp_d {A: Type} {JA: Join A} {SA: Sep_alg A} {PA : Perm_alg A} {CA: Canc_alg A}: forall P, disjointed P emp.
proof: Proof. intros. unfold disjointed. simpl; intros. pose proof split_identity _ _ H0 H2. pose proof split_identity _ _ (join_comm H0) H2. pose proof identities_unique H3 H4 (ex_intro _ h23 H0). subst. split; eauto. Qed.
imports: CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext VST.msl.msl_direct CertiGraph.msl_ext.sepalg