Require Import VST.msl.Extensionality.
Require Import VST.msl.seplog.
Require Import VST.msl.base.
Require Import VST.msl.boolean_alg.
Require Import VST.msl.sepalg.
Require Import VST.msl.predicates_sa.
Require Import VST.msl.corable_direct.

Local Open Scope logic.

Instance algNatDed (T: Type) : NatDed (pred T).
  apply (mkNatDed _
                    predicates_sa.andp
                    predicates_sa.orp
                    (@predicates_sa.exp _)
                    (@predicates_sa.allp _)
                    predicates_sa.imp predicates_sa.prop
                    (@predicates_sa.derives _)).
(* Goal: forall (P Q : pred T) (_ : @derives T P Q) (_ : @derives T Q P), @eq (pred T) P Q *)
(* Goal: forall P : pred T, @derives T P P *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P Q) (_ : @derives T Q R), @derives T P R *)
(* Goal: forall (X P Q : pred T) (_ : @derives T X P) (_ : @derives T X Q), @derives T X (@andp T P Q) *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R), @derives T (@andp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T Q R), @derives T (@andp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R) (_ : @derives T Q R), @derives T (@orp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P Q), @derives T P (@orp T Q R) *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R), @derives T P (@orp T Q R) *)
(* Goal: forall (B : Type) (x : B) (P : pred T) (Q : forall _ : B, pred T) (_ : @derives T P (Q x)), @derives T P (@exp T B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (Q : pred T) (_ : forall x : B, @derives T (P x) Q), @derives T (@exp T B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (x : B) (Q : pred T) (_ : @derives T (P x) Q), @derives T (@allp T B P) Q *)
(* Goal: forall (B : Type) (P : pred T) (Q : forall _ : B, pred T) (_ : forall v : B, @derives T P (Q v)), @derives T P (@allp T B Q) *)
(* Goal: forall P Q R : pred T, iff (@derives T (@andp T P Q) R) (@derives T P (@imp T Q R)) *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : forall _ : P, @derives T (@prop T True) Q), @derives T (@prop T P) Q *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : P), @derives T Q (@prop T P) *)
(* Goal: forall P Q : Prop, @derives T (@imp T (@prop T P) (@prop T Q)) (@prop T (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 apply pred_ext.
(* Goal: forall P : pred T, @derives T P P *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P Q) (_ : @derives T Q R), @derives T P R *)
(* Goal: forall (X P Q : pred T) (_ : @derives T X P) (_ : @derives T X Q), @derives T X (@andp T P Q) *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R), @derives T (@andp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T Q R), @derives T (@andp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R) (_ : @derives T Q R), @derives T (@orp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P Q), @derives T P (@orp T Q R) *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R), @derives T P (@orp T Q R) *)
(* Goal: forall (B : Type) (x : B) (P : pred T) (Q : forall _ : B, pred T) (_ : @derives T P (Q x)), @derives T P (@exp T B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (Q : pred T) (_ : forall x : B, @derives T (P x) Q), @derives T (@exp T B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (x : B) (Q : pred T) (_ : @derives T (P x) Q), @derives T (@allp T B P) Q *)
(* Goal: forall (B : Type) (P : pred T) (Q : forall _ : B, pred T) (_ : forall v : B, @derives T P (Q v)), @derives T P (@allp T B Q) *)
(* Goal: forall P Q R : pred T, iff (@derives T (@andp T P Q) R) (@derives T P (@imp T Q R)) *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : forall _ : P, @derives T (@prop T True) Q), @derives T (@prop T P) Q *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : P), @derives T Q (@prop T P) *)
(* Goal: forall P Q : Prop, @derives T (@imp T (@prop T P) (@prop T Q)) (@prop T (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 apply derives_refl.
(* Goal: forall (P Q R : pred T) (_ : @derives T P Q) (_ : @derives T Q R), @derives T P R *)
(* Goal: forall (X P Q : pred T) (_ : @derives T X P) (_ : @derives T X Q), @derives T X (@andp T P Q) *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R), @derives T (@andp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T Q R), @derives T (@andp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R) (_ : @derives T Q R), @derives T (@orp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P Q), @derives T P (@orp T Q R) *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R), @derives T P (@orp T Q R) *)
(* Goal: forall (B : Type) (x : B) (P : pred T) (Q : forall _ : B, pred T) (_ : @derives T P (Q x)), @derives T P (@exp T B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (Q : pred T) (_ : forall x : B, @derives T (P x) Q), @derives T (@exp T B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (x : B) (Q : pred T) (_ : @derives T (P x) Q), @derives T (@allp T B P) Q *)
(* Goal: forall (B : Type) (P : pred T) (Q : forall _ : B, pred T) (_ : forall v : B, @derives T P (Q v)), @derives T P (@allp T B Q) *)
(* Goal: forall P Q R : pred T, iff (@derives T (@andp T P Q) R) (@derives T P (@imp T Q R)) *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : forall _ : P, @derives T (@prop T True) Q), @derives T (@prop T P) Q *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : P), @derives T Q (@prop T P) *)
(* Goal: forall P Q : Prop, @derives T (@imp T (@prop T P) (@prop T Q)) (@prop T (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 apply derives_trans.
(* Goal: forall (X P Q : pred T) (_ : @derives T X P) (_ : @derives T X Q), @derives T X (@andp T P Q) *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R), @derives T (@andp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T Q R), @derives T (@andp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R) (_ : @derives T Q R), @derives T (@orp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P Q), @derives T P (@orp T Q R) *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R), @derives T P (@orp T Q R) *)
(* Goal: forall (B : Type) (x : B) (P : pred T) (Q : forall _ : B, pred T) (_ : @derives T P (Q x)), @derives T P (@exp T B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (Q : pred T) (_ : forall x : B, @derives T (P x) Q), @derives T (@exp T B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (x : B) (Q : pred T) (_ : @derives T (P x) Q), @derives T (@allp T B P) Q *)
(* Goal: forall (B : Type) (P : pred T) (Q : forall _ : B, pred T) (_ : forall v : B, @derives T P (Q v)), @derives T P (@allp T B Q) *)
(* Goal: forall P Q R : pred T, iff (@derives T (@andp T P Q) R) (@derives T P (@imp T Q R)) *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : forall _ : P, @derives T (@prop T True) Q), @derives T (@prop T P) Q *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : P), @derives T Q (@prop T P) *)
(* Goal: forall P Q : Prop, @derives T (@imp T (@prop T P) (@prop T Q)) (@prop T (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 apply andp_right.
(* Goal: forall (P Q R : pred T) (_ : @derives T P R), @derives T (@andp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T Q R), @derives T (@andp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R) (_ : @derives T Q R), @derives T (@orp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P Q), @derives T P (@orp T Q R) *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R), @derives T P (@orp T Q R) *)
(* Goal: forall (B : Type) (x : B) (P : pred T) (Q : forall _ : B, pred T) (_ : @derives T P (Q x)), @derives T P (@exp T B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (Q : pred T) (_ : forall x : B, @derives T (P x) Q), @derives T (@exp T B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (x : B) (Q : pred T) (_ : @derives T (P x) Q), @derives T (@allp T B P) Q *)
(* Goal: forall (B : Type) (P : pred T) (Q : forall _ : B, pred T) (_ : forall v : B, @derives T P (Q v)), @derives T P (@allp T B Q) *)
(* Goal: forall P Q R : pred T, iff (@derives T (@andp T P Q) R) (@derives T P (@imp T Q R)) *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : forall _ : P, @derives T (@prop T True) Q), @derives T (@prop T P) Q *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : P), @derives T Q (@prop T P) *)
(* Goal: forall P Q : Prop, @derives T (@imp T (@prop T P) (@prop T Q)) (@prop T (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 apply andp_left1.
(* Goal: forall (P Q R : pred T) (_ : @derives T Q R), @derives T (@andp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R) (_ : @derives T Q R), @derives T (@orp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P Q), @derives T P (@orp T Q R) *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R), @derives T P (@orp T Q R) *)
(* Goal: forall (B : Type) (x : B) (P : pred T) (Q : forall _ : B, pred T) (_ : @derives T P (Q x)), @derives T P (@exp T B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (Q : pred T) (_ : forall x : B, @derives T (P x) Q), @derives T (@exp T B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (x : B) (Q : pred T) (_ : @derives T (P x) Q), @derives T (@allp T B P) Q *)
(* Goal: forall (B : Type) (P : pred T) (Q : forall _ : B, pred T) (_ : forall v : B, @derives T P (Q v)), @derives T P (@allp T B Q) *)
(* Goal: forall P Q R : pred T, iff (@derives T (@andp T P Q) R) (@derives T P (@imp T Q R)) *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : forall _ : P, @derives T (@prop T True) Q), @derives T (@prop T P) Q *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : P), @derives T Q (@prop T P) *)
(* Goal: forall P Q : Prop, @derives T (@imp T (@prop T P) (@prop T Q)) (@prop T (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 apply andp_left2.
(* Goal: forall (P Q R : pred T) (_ : @derives T P R) (_ : @derives T Q R), @derives T (@orp T P Q) R *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P Q), @derives T P (@orp T Q R) *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R), @derives T P (@orp T Q R) *)
(* Goal: forall (B : Type) (x : B) (P : pred T) (Q : forall _ : B, pred T) (_ : @derives T P (Q x)), @derives T P (@exp T B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (Q : pred T) (_ : forall x : B, @derives T (P x) Q), @derives T (@exp T B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (x : B) (Q : pred T) (_ : @derives T (P x) Q), @derives T (@allp T B P) Q *)
(* Goal: forall (B : Type) (P : pred T) (Q : forall _ : B, pred T) (_ : forall v : B, @derives T P (Q v)), @derives T P (@allp T B Q) *)
(* Goal: forall P Q R : pred T, iff (@derives T (@andp T P Q) R) (@derives T P (@imp T Q R)) *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : forall _ : P, @derives T (@prop T True) Q), @derives T (@prop T P) Q *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : P), @derives T Q (@prop T P) *)
(* Goal: forall P Q : Prop, @derives T (@imp T (@prop T P) (@prop T Q)) (@prop T (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 apply orp_left.
(* Goal: forall (P Q R : pred T) (_ : @derives T P Q), @derives T P (@orp T Q R) *)
(* Goal: forall (P Q R : pred T) (_ : @derives T P R), @derives T P (@orp T Q R) *)
(* Goal: forall (B : Type) (x : B) (P : pred T) (Q : forall _ : B, pred T) (_ : @derives T P (Q x)), @derives T P (@exp T B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (Q : pred T) (_ : forall x : B, @derives T (P x) Q), @derives T (@exp T B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (x : B) (Q : pred T) (_ : @derives T (P x) Q), @derives T (@allp T B P) Q *)
(* Goal: forall (B : Type) (P : pred T) (Q : forall _ : B, pred T) (_ : forall v : B, @derives T P (Q v)), @derives T P (@allp T B Q) *)
(* Goal: forall P Q R : pred T, iff (@derives T (@andp T P Q) R) (@derives T P (@imp T Q R)) *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : forall _ : P, @derives T (@prop T True) Q), @derives T (@prop T P) Q *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : P), @derives T Q (@prop T P) *)
(* Goal: forall P Q : Prop, @derives T (@imp T (@prop T P) (@prop T Q)) (@prop T (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 apply orp_right1.
(* Goal: forall (P Q R : pred T) (_ : @derives T P R), @derives T P (@orp T Q R) *)
(* Goal: forall (B : Type) (x : B) (P : pred T) (Q : forall _ : B, pred T) (_ : @derives T P (Q x)), @derives T P (@exp T B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (Q : pred T) (_ : forall x : B, @derives T (P x) Q), @derives T (@exp T B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (x : B) (Q : pred T) (_ : @derives T (P x) Q), @derives T (@allp T B P) Q *)
(* Goal: forall (B : Type) (P : pred T) (Q : forall _ : B, pred T) (_ : forall v : B, @derives T P (Q v)), @derives T P (@allp T B Q) *)
(* Goal: forall P Q R : pred T, iff (@derives T (@andp T P Q) R) (@derives T P (@imp T Q R)) *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : forall _ : P, @derives T (@prop T True) Q), @derives T (@prop T P) Q *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : P), @derives T Q (@prop T P) *)
(* Goal: forall P Q : Prop, @derives T (@imp T (@prop T P) (@prop T Q)) (@prop T (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 apply orp_right2.
(* Goal: forall (B : Type) (x : B) (P : pred T) (Q : forall _ : B, pred T) (_ : @derives T P (Q x)), @derives T P (@exp T B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (Q : pred T) (_ : forall x : B, @derives T (P x) Q), @derives T (@exp T B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (x : B) (Q : pred T) (_ : @derives T (P x) Q), @derives T (@allp T B P) Q *)
(* Goal: forall (B : Type) (P : pred T) (Q : forall _ : B, pred T) (_ : forall v : B, @derives T P (Q v)), @derives T P (@allp T B Q) *)
(* Goal: forall P Q R : pred T, iff (@derives T (@andp T P Q) R) (@derives T P (@imp T Q R)) *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : forall _ : P, @derives T (@prop T True) Q), @derives T (@prop T P) Q *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : P), @derives T Q (@prop T P) *)
(* Goal: forall P Q : Prop, @derives T (@imp T (@prop T P) (@prop T Q)) (@prop T (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 intros ? ?; apply @exp_right.
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (Q : pred T) (_ : forall x : B, @derives T (P x) Q), @derives T (@exp T B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (x : B) (Q : pred T) (_ : @derives T (P x) Q), @derives T (@allp T B P) Q *)
(* Goal: forall (B : Type) (P : pred T) (Q : forall _ : B, pred T) (_ : forall v : B, @derives T P (Q v)), @derives T P (@allp T B Q) *)
(* Goal: forall P Q R : pred T, iff (@derives T (@andp T P Q) R) (@derives T P (@imp T Q R)) *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : forall _ : P, @derives T (@prop T True) Q), @derives T (@prop T P) Q *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : P), @derives T Q (@prop T P) *)
(* Goal: forall P Q : Prop, @derives T (@imp T (@prop T P) (@prop T Q)) (@prop T (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 intros ? ?; apply @exp_left.
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (x : B) (Q : pred T) (_ : @derives T (P x) Q), @derives T (@allp T B P) Q *)
(* Goal: forall (B : Type) (P : pred T) (Q : forall _ : B, pred T) (_ : forall v : B, @derives T P (Q v)), @derives T P (@allp T B Q) *)
(* Goal: forall P Q R : pred T, iff (@derives T (@andp T P Q) R) (@derives T P (@imp T Q R)) *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : forall _ : P, @derives T (@prop T True) Q), @derives T (@prop T P) Q *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : P), @derives T Q (@prop T P) *)
(* Goal: forall P Q : Prop, @derives T (@imp T (@prop T P) (@prop T Q)) (@prop T (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 intros ? ?; apply @allp_left.
(* Goal: forall (B : Type) (P : pred T) (Q : forall _ : B, pred T) (_ : forall v : B, @derives T P (Q v)), @derives T P (@allp T B Q) *)
(* Goal: forall P Q R : pred T, iff (@derives T (@andp T P Q) R) (@derives T P (@imp T Q R)) *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : forall _ : P, @derives T (@prop T True) Q), @derives T (@prop T P) Q *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : P), @derives T Q (@prop T P) *)
(* Goal: forall P Q : Prop, @derives T (@imp T (@prop T P) (@prop T Q)) (@prop T (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 intros ? ?; apply @allp_right.
(* Goal: forall P Q R : pred T, iff (@derives T (@andp T P Q) R) (@derives T P (@imp T Q R)) *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : forall _ : P, @derives T (@prop T True) Q), @derives T (@prop T P) Q *)
(* Goal: forall (P : Prop) (Q : pred T) (_ : P), @derives T Q (@prop T P) *)
(* Goal: forall P Q : Prop, @derives T (@imp T (@prop T P) (@prop T Q)) (@prop T (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 apply imp_andp_adjoint.
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 repeat intro. eapply H; eauto.
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 repeat intro. hnf; auto.
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 repeat intro. unfold imp, prop in H. auto.
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T (@allp T B (fun b : B => @prop T (P b))) (@prop T (forall b : B, P b)) *)
 repeat intro. specialize (H b); unfold prop in H. auto.
Defined.

Instance algSepLog (T: Type) {JoinT: Join T}{PermT: Perm_alg T}{SepT: Sep_alg T} :
      @SepLog (pred T) (algNatDed T).
 apply (mkSepLog _ (algNatDed T) identity predicates_sa.sepcon predicates_sa.wand
                             predicates_sa.ewand).
(* Goal: forall P Q R : pred T, @eq (pred T) (@sepcon T JoinT (@sepcon T JoinT P Q) R) (@sepcon T JoinT P (@sepcon T JoinT Q R)) *)
(* Goal: forall P Q : pred T, @eq (pred T) (@sepcon T JoinT P Q) (@sepcon T JoinT Q P) *)
(* Goal: forall P Q R : pred T, iff (@seplog.derives (pred T) (algNatDed T) (@sepcon T JoinT P Q) R) (@seplog.derives (pred T) (algNatDed T) P (@wand T JoinT Q R)) *)
(* Goal: forall (P : pred T) (Q : Prop) (R : pred T), @eq (pred T) (@sepcon T JoinT P (@seplog.andp (pred T) (algNatDed T) (@seplog.prop (pred T) (algNatDed T) Q) R)) (@seplog.andp (pred T) (algNatDed T) (@seplog.prop (pred T) (algNatDed T) Q) (@sepcon T JoinT P R)) *)
(* Goal: forall (P P' Q Q' : pred T) (_ : @seplog.derives (pred T) (algNatDed T) P P') (_ : @seplog.derives (pred T) (algNatDed T) Q Q'), @seplog.derives (pred T) (algNatDed T) (@sepcon T JoinT P Q) (@sepcon T JoinT P' Q') *)
(* Goal: forall P Q R : pred T, @eq (pred T) (@ewand T JoinT (@sepcon T JoinT P Q) R) (@ewand T JoinT P (@ewand T JoinT Q R)) *)
(* Goal: forall P Q R : pred T, @seplog.derives (pred T) (algNatDed T) (@seplog.andp (pred T) (algNatDed T) (@sepcon T JoinT P Q) (@ewand T JoinT R (@seplog.TT (pred T) (algNatDed T)))) (@sepcon T JoinT (@seplog.andp (pred T) (algNatDed T) P (@ewand T JoinT R (@seplog.TT (pred T) (algNatDed T)))) (@seplog.andp (pred T) (algNatDed T) Q (@ewand T JoinT R (@seplog.TT (pred T) (algNatDed T))))) *)
(* Goal: forall P Q : pred T, @seplog.derives (pred T) (algNatDed T) (@sepcon T JoinT P Q) (@sepcon T JoinT (@seplog.andp (pred T) (algNatDed T) P (@ewand T JoinT Q (@seplog.TT (pred T) (algNatDed T)))) Q) *)
(* Goal: forall (P Q R : pred T) (_ : @seplog.derives (pred T) (algNatDed T) (@sepcon T JoinT P Q) (@seplog.FF (pred T) (algNatDed T))), @seplog.derives (pred T) (algNatDed T) (@seplog.andp (pred T) (algNatDed T) P (@ewand T JoinT Q R)) (@seplog.FF (pred T) (algNatDed T)) *)
 apply sepcon_assoc.
(* Goal: forall P Q : pred T, @eq (pred T) (@sepcon T JoinT P Q) (@sepcon T JoinT Q P) *)
(* Goal: forall P Q R : pred T, iff (@seplog.derives (pred T) (algNatDed T) (@sepcon T JoinT P Q) R) (@seplog.derives (pred T) (algNatDed T) P (@wand T JoinT Q R)) *)
(* Goal: forall (P : pred T) (Q : Prop) (R : pred T), @eq (pred T) (@sepcon T JoinT P (@seplog.andp (pred T) (algNatDed T) (@seplog.prop (pred T) (algNatDed T) Q) R)) (@seplog.andp (pred T) (algNatDed T) (@seplog.prop (pred T) (algNatDed T) Q) (@sepcon T JoinT P R)) *)
(* Goal: forall (P P' Q Q' : pred T) (_ : @seplog.derives (pred T) (algNatDed T) P P') (_ : @seplog.derives (pred T) (algNatDed T) Q Q'), @seplog.derives (pred T) (algNatDed T) (@sepcon T JoinT P Q) (@sepcon T JoinT P' Q') *)
(* Goal: forall P Q R : pred T, @eq (pred T) (@ewand T JoinT (@sepcon T JoinT P Q) R) (@ewand T JoinT P (@ewand T JoinT Q R)) *)
(* Goal: forall P Q R : pred T, @seplog.derives (pred T) (algNatDed T) (@seplog.andp (pred T) (algNatDed T) (@sepcon T JoinT P Q) (@ewand T JoinT R (@seplog.TT (pred T) (algNatDed T)))) (@sepcon T JoinT (@seplog.andp (pred T) (algNatDed T) P (@ewand T JoinT R (@seplog.TT (pred T) (algNatDed T)))) (@seplog.andp (pred T) (algNatDed T) Q (@ewand T JoinT R (@seplog.TT (pred T) (algNatDed T))))) *)
(* Goal: forall P Q : pred T, @seplog.derives (pred T) (algNatDed T) (@sepcon T JoinT P Q) (@sepcon T JoinT (@seplog.andp (pred T) (algNatDed T) P (@ewand T JoinT Q (@seplog.TT (pred T) (algNatDed T)))) Q) *)
(* Goal: forall (P Q R : pred T) (_ : @seplog.derives (pred T) (algNatDed T) (@sepcon T JoinT P Q) (@seplog.FF (pred T) (algNatDed T))), @seplog.derives (pred T) (algNatDed T) (@seplog.andp (pred T) (algNatDed T) P (@ewand T JoinT Q R)) (@seplog.FF (pred T) (algNatDed T)) *)
 apply sepcon_comm.
(* Goal: P b *)
 intros. pose proof (wand_sepcon_adjoint P Q R). simpl. rewrite H; split; auto.
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (_ : forall b : B, @corable T JoinT PermT SepT (P b)), @corable T JoinT PermT SepT (@allp T B P) *)
 intros. apply (predicates_sa.sepcon_andp_prop P Q R).
(* Goal: P b *)
 intros; intro; apply sepcon_derives; auto.
(* Goal: forall P Q R : pred T, @eq (pred T) (@ewand T JoinT (@sepcon T JoinT P Q) R) (@ewand T JoinT P (@ewand T JoinT Q R)) *)
(* Goal: forall P Q R : pred T, @seplog.derives (pred T) (algNatDed T) (@seplog.andp (pred T) (algNatDed T) (@sepcon T JoinT P Q) (@ewand T JoinT R (@seplog.TT (pred T) (algNatDed T)))) (@sepcon T JoinT (@seplog.andp (pred T) (algNatDed T) P (@ewand T JoinT R (@seplog.TT (pred T) (algNatDed T)))) (@seplog.andp (pred T) (algNatDed T) Q (@ewand T JoinT R (@seplog.TT (pred T) (algNatDed T))))) *)
(* Goal: forall P Q : pred T, @seplog.derives (pred T) (algNatDed T) (@sepcon T JoinT P Q) (@sepcon T JoinT (@seplog.andp (pred T) (algNatDed T) P (@ewand T JoinT Q (@seplog.TT (pred T) (algNatDed T)))) Q) *)
(* Goal: forall (P Q R : pred T) (_ : @seplog.derives (pred T) (algNatDed T) (@sepcon T JoinT P Q) (@seplog.FF (pred T) (algNatDed T))), @seplog.derives (pred T) (algNatDed T) (@seplog.andp (pred T) (algNatDed T) P (@ewand T JoinT Q R)) (@seplog.FF (pred T) (algNatDed T)) *)
 intros; apply predicates_sa.ewand_sepcon.
(* Goal: P b *)
 intros; simpl. apply ewand_TT_sepcon; auto.
(* Goal: P b *)
 intros; simpl. intros w [w1 [w2 [? [? ?]]]]. exists w1,w2; repeat split; auto. exists w2; exists w; repeat split; auto.
(* Goal: P b *)
 intros; simpl. apply ewand_conflict; auto.
Defined.

Instance algClassicalSep (T: Type) {JoinT: Join T}{PermT: Perm_alg T}{SepT: Sep_alg T}{CancT: Canc_alg T}:
     @ClassicalSep (pred T) (algNatDed T)(algSepLog T).
(* Goal: forall (B : Type) (P : forall _ : B, pred T) (_ : forall b : B, @corable T JoinT PermT SepT (P b)), @corable T JoinT PermT SepT (@allp T B P) *)
 constructor; intros. simpl. apply predicates_sa.sepcon_emp.
Defined.

Instance algCorableSepLog (T: Type){JoinT: Join T}{PermT: Perm_alg T}{SepT: Sep_alg T}:
         @CorableSepLog (pred T) (algNatDed T) (algSepLog T).
(* Goal: @eq (pred T) (@seplog.sepcon (pred T) (algNatDed T) (@algSepLog T JoinT PermT SepT) P (@emp (pred T) (algNatDed T) (@algSepLog T JoinT PermT SepT))) P *)
  apply mkCorableSepLog with (corable := corable_direct.corable); unfold algNatDed, algSepLog; simpl.
  + apply corable_prop.
  + apply corable_andp.
  + apply corable_orp.
  + apply corable_imp.
(* Goal: P b *)
  + intros. apply corable_allp; auto.
(* Goal: P b *)
  + intros; apply corable_exp; auto.
  + apply corable_sepcon.
  + apply corable_wand.
(* Goal: @eq (pred T) (@seplog.sepcon (pred T) (algNatDed T) (@algSepLog T JoinT PermT SepT) P (@emp (pred T) (algNatDed T) (@algSepLog T JoinT PermT SepT))) P *)
  + intros; simpl.
(* Goal: P b *)
    apply corable_andp_sepcon1; auto.
Defined.
