proposition: Lemma precise_sepcon_i {A} {JA : Join A} {PA : Perm_alg A} {SA: Sep_alg A} {AG : ageable A} {AA: Age_alg A}: forall P Q, precise Q -> precise P -> precise (P * Q).
proof: Proof. repeat intro; destruct H1 as [w11 [w12 [? [? ?]]]], H2 as [w21 [w22 [? [? ?]]]]. assert (w11 = w21) by (apply join_join_sub in H1; generalize (join_sub_trans H1 H3); intro; apply join_join_sub in H2; generalize (join_sub_trans H2 H4); intro; hnf in H0; apply H0 with (w := w); trivial). assert (w12 = w22) by (apply join_join_sub' in H1; generalize (join_sub_trans H1 H3); intro; apply join_join_sub' in H2; generalize (join_sub_trans H2 H4); intro; hnf in H; apply H with (w := w); trivial). rewrite H9 in *; rewrite H10 in *; equate_join w1 w2; auto. Qed.
imports: VST.msl.msl_standard CertiGraph.msl_ext.ramify_tactics