proposition: Lemma precise_ocon_d {A} {JA : Join A} {PA : Perm_alg A} {SA: Sep_alg A}{CaA : Canc_alg A}{CrA : Cross_alg A}{DA : Disj_alg A} : forall P Q, precise P -> precise Q -> precise (P ⊗ Q).
proof: Proof. intros; intro; intros. destruct_ocon H1 h; destruct_ocon H2 i. generalize (join_join_sub H6); intro; generalize (join_sub_trans H13 H3); intro. generalize (join_join_sub H10); intro; generalize (join_sub_trans H15 H4); intro. generalize (H w h12 i12 H7 H11 H14 H16); intro. try_join h2 h3 h23'; equate_join h23 h23'; try_join i2 i3 i23'; equate_join i23 i23'. generalize (join_join_sub' H19); intro; generalize (join_sub_trans H18 H3); intro. generalize (join_join_sub' H20); intro; generalize (join_sub_trans H22 H4); intro. generalize (H0 w h23 i23 H8 H12 H21 H23); intro. rewrite H17 in *; rewrite H24 in *. clear h12 h23 H7 H8 H11 H12 H13 H14 H15 H16 H17 H18 H21 H22 H23 H24. apply (overlapping_eq h1 h2 h3 i1 i2 i3 i12 i23); trivial. Qed.
imports: CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext VST.msl.msl_direct CertiGraph.msl_ext.sepalg