proposition: Lemma join_necR {A}{JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A}: forall h1 h2 h12 h1' h2' h12', join h1 h2 h12 -> join h1' h2' h12' -> necR h1 h1' -> necR h2 h2' -> necR h12 h12'.
proof: Proof. intros; destruct (nec_join H H1) as [w2 [w12 [? [? ?]]]]; destruct (join_level _ _ _ H3); rewrite <- H7 in H6; destruct (join_level _ _ _ H0); rewrite <- H9 in H8; rewrite H8 in H6; generalize (necR_linear' H2 H4 H6); intro; rewrite <- H10 in H3; equate_join h12' w12; auto. Qed.
imports: VST.msl.msl_standard VST.msl.corable CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext CertiGraph.msl_ext.sepalg