proposition: Lemma precise_ocon_contain_d {A} {JA: Join A} {PA: Perm_alg A} {SA: Sep_alg A} {CA: Canc_alg A} {DA: Disj_alg A} : forall P Q, precise P -> Q |-- P * TT -> Q = ocon P Q.
proof: Proof. intros; apply pred_ext; [apply ocon_contain_d; auto |]. unfold ocon, owand, derives in *; simpl in *. intros. destruct H1 as [h1 [h2 [h3 [h12 [h23 [? [? [? [? ?]]]]]]]]]. destruct (H0 _ H5) as [y [z [? [? ?]]]]. try_join h2 h3 h23'. equate_join h23 h23'. assertSub y a HS1. equate_precise_direct y h12. try_join z h1 h3'. equate_canc h3 h3'. assert (identity h1). 1: { try_join h1 h3 h_temp. assertSub h1 h3 H12. eapply join_sub_joins_identity; eauto. } apply join_comm in H4. apply H9 in H10; apply H9 in H4. subst. auto. Qed.
imports: CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext VST.msl.msl_direct CertiGraph.msl_ext.sepalg