proposition: Lemma ocon_derives_i {A} {JA: Join A}{PA: Perm_alg A}{AG : ageable A} {AA : Age_alg A}: forall p q p' q', (p |-- p') -> (q |-- q') -> (p ⊗ q |-- p' ⊗ q').
proof: Proof. repeat (intros; hnf). simpl in H1. destruct_ocon H1 w. exists w1,w2,w3,w12,w23. repeat split; auto. Qed.
imports: VST.msl.msl_standard VST.msl.corable CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext CertiGraph.msl_ext.sepalg