proposition: Lemma cross_rev_d {A}{JA: Join A}{PA: Perm_alg A}: forall h1 h2 h3 h4 h12 h34 h13 h24 h1234, join h1 h2 h12 -> join h1 h3 h13 -> join h3 h4 h34 -> join h2 h4 h24 -> join h12 h34 h1234 -> join h13 h24 h1234.
proof: Proof. intros; try_join h2 h34 h234; try_join h2 h4 h24'; equate_join h24 h24'; try_join h1 h3 h13'; equate_join h13 h13'; auto. Qed.
imports: CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext VST.msl.msl_direct CertiGraph.msl_ext.sepalg