proposition: Lemma join_identity {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}: forall a b c, join a b c -> identity a -> identity b -> identity c.
proof: Proof. intros. hnf; intros x y ?. try_join b x bx. apply H1 in H3. apply H0 in H4. subst; auto. Qed.
imports: VST.msl.Extensionality VST.msl.sepalg CertiGraph.msl_ext.abs_addr CertiGraph.msl_ext.ramify_tactics