proposition: Lemma disj_emp_i {A: Type} {JA: Join A} {SA: Sep_alg A} {PA : Perm_alg A} {AG : ageable A} {AA : Age_alg A}: forall P, disjointed P emp.
proof: Proof. intros. unfold disjointed, emp; 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: VST.msl.msl_standard VST.msl.corable CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext CertiGraph.msl_ext.sepalg