proposition: Lemma overlapping_join_eq {A} {JA : Join A} {PA : Perm_alg A} {SA: Sep_alg A} {DA : Disj_alg A}: forall h1 h2 h3 h4 h12 h23 w, join h1 h2 h12 -> join h2 h3 h23 -> join h12 h3 w -> join h12 h4 h23 -> h23 = w.
proof: Proof. intros. try_join h2 h3 h23'; equate_join h23 h23'. assertSub h1 h23 HS. assert (identity h1). apply join_sub_joins_identity with h23; auto. exists w; auto. apply join_unit1_e with h1; auto. Qed.
imports: VST.msl.msl_standard CertiGraph.msl_ext.ramify_tactics Coq.Sorting.Permutation