proposition: Lemma ocon_sep_true_d {A}{JA: Join A}{PA: Perm_alg A}: forall P Q, P ⊗ Q |-- P * TT.
proof: Proof. intros; hnf; intros; simpl in *; intros. destruct_ocon H h. exists h12, h3. repeat split; auto. Qed.
imports: CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext VST.msl.msl_direct CertiGraph.msl_ext.sepalg