proposition: Lemma contravariant_ocon {B}{A} {JA: Join A}{PA: Perm_alg A}{AG : ageable A} {AA : Age_alg A}: forall F1 F2 : (B -> pred A) -> (B -> pred A), contravariant F1 -> contravariant F2 -> contravariant (fun (x : B -> pred A) b => F1 x b ⊗ F2 x b).
proof: Proof. intros; hnf. intros P Q ? ?. eapply ocon_derives_i. apply H, H1. apply H0, H1. Qed.
imports: VST.msl.msl_standard VST.msl.corable CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext CertiGraph.msl_ext.sepalg