proposition: Lemma precise_left_sepcon_andp_distr_d {A} {JA : Join A} {PA : Perm_alg A} {SA: Sep_alg A} {CA : Canc_alg A}: forall P P1 P2 Q R, precise P -> P1 |-- P -> P2 |-- P -> (P1 * Q) && (P2 * R) |-- (P1 && P2) * (Q && R).
proof: Proof. intros. unfold sepcon, andp, derives; simpl. intros. destruct H2 as [[?y [?z [? [? ?]]]] [?y [?z [? [? ?]]]]]. exists y, z. assert (P y) by auto. assert (P y0) by auto. equate_precise_direct y y0. equate_canc z z0. repeat split; auto. Qed.
imports: VST.msl.msl_direct CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.overlapping_direct VST.msl.predicates_sa