Require Import VST.msl.Extensionality.

Class NatDed (A: Type) := mkNatDed {
  andp: A -> A -> A;
  orp: A -> A -> A;
  exp: forall {T:Type}, (T -> A) -> A;
  allp: forall {T:Type}, (T -> A) -> A;
  imp: A -> A -> A;
  prop: Prop -> A;
  derives: A -> A -> Prop;
  pred_ext: forall P Q, derives P Q -> derives Q P -> P=Q;
  derives_refl: forall P, derives P P;
  derives_trans: forall P Q R, derives P Q -> derives Q R -> derives P R;
  TT := prop True;
  FF := prop False;
  andp_right:  forall X P Q:A, derives X P -> derives X Q -> derives X (andp P Q);
  andp_left1:  forall P Q R:A, derives P R -> derives (andp P Q) R;
  andp_left2:  forall P Q R:A, derives Q R -> derives (andp P Q) R;
  orp_left: forall P Q R, derives P R -> derives Q R -> derives (orp P Q) R;
  orp_right1: forall P Q R, derives P Q -> derives P (orp Q R);
  orp_right2: forall P Q R, derives P R -> derives P (orp Q R);
  exp_right: forall {B: Type} (x:B) (P: A) (Q: B -> A),
                        derives P (Q x) -> derives P (exp Q);
  exp_left: forall {B: Type} (P: B -> A) (Q: A),
                      (forall x, derives (P x) Q) -> derives (exp P) Q;
  allp_left: forall {B}(P: B -> A) x Q, derives (P x) Q -> derives (allp P) Q;
  allp_right: forall {B}(P: A) (Q: B -> A),  (forall v, derives P (Q v)) -> derives P (allp Q);
  imp_andp_adjoint: forall P Q R, derives (andp P Q) R <-> derives P (imp Q R);
  prop_left: forall (P: Prop) Q, (P -> derives TT Q) -> derives (prop P) Q;
  prop_right: forall (P: Prop) Q, P -> derives Q (prop P);
  prop_imp_prop_left: forall (P Q: Prop), derives (imp (prop P) (prop Q)) (prop (P -> Q));
  allp_prop_left: forall {B: Type} (P: B -> Prop), derives (allp (fun b => prop (P b))) (prop (forall b, P b))
(* not_prop_right: forall (P: A) (Q: Prop), (Q -> derives P FF) -> derives P (prop (not Q)) *)
}.

Program Instance LiftNatDed (A B: Type) {ND: NatDed B} : NatDed (A -> B) :=
 mkNatDed (A -> B)
    (*andp*) (fun P Q x => andp (P x) (Q x))
    (*orp*) (fun P Q x => orp (P x) (Q x))
    (*exp*) (fun {T} (F: T -> A -> B) (a: A) => exp (fun x => F x a))
    (*allp*) (fun {T} (F: T -> A -> B) (a: A) => allp (fun x => F x a))
    (*imp*) (fun P Q x => imp (P x) (Q x))
    (*prop*) (fun P x => prop P)
    (*derives*) (fun P Q => forall x, derives (P x) (Q x))
     _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _.
Next Obligation.
(* Goal: @eq (forall _ : A, B) P Q *)
 intros; extensionality x; apply pred_ext; auto.
Defined.
Next Obligation.
(* Goal: @derives B ND (P x) (P x) *)
 intros; apply derives_refl.
Defined.
Next Obligation.
(* Goal: @derives B ND (P x) (R x) *)
 intros; eapply derives_trans; eauto.
Defined.
Next Obligation.
(* Goal: @derives B ND (X x) (@andp B ND (P x) (Q x)) *)
 intros; eapply andp_right; eauto.
Defined.
Next Obligation.
(* Goal: @derives B ND (@andp B ND (P x) (Q x)) (R x) *)
 intros; eapply andp_left1; eauto.
Defined.
Next Obligation.
(* Goal: @derives B ND (@andp B ND (P x) (Q x)) (R x) *)
 intros; eapply andp_left2; eauto.
Defined.
Next Obligation.
(* Goal: @derives B ND (@orp B ND (P x) (Q x)) (R x) *)
 intros; eapply orp_left; eauto.
Defined.
Next Obligation.
(* Goal: @derives B ND (P x) (@orp B ND (Q x) (R x)) *)
 intros; eapply orp_right1; eauto.
Defined.
Next Obligation.
(* Goal: @derives B ND (P x) (@orp B ND (Q x) (R x)) *)
 intros; eapply orp_right2; eauto.
Defined.
Next Obligation.
(* Goal: @derives B ND (P x0) (@exp B ND B0 (fun x : B0 => Q x x0)) *)
 intros; eapply exp_right; eauto.
Defined.
Next Obligation.
(* Goal: @derives B ND (@exp B ND B0 (fun x0 : B0 => P x0 x)) (Q x) *)
 intros; eapply exp_left; eauto.
Defined.
Next Obligation.
(* Goal: @derives B ND (@allp B ND B0 (fun x : B0 => P x x0)) (Q x0) *)
 intros; eapply allp_left; eauto.
Defined.
Next Obligation.
(* Goal: @derives B ND (P x) (@allp B ND B0 (fun x0 : B0 => Q x0 x)) *)
 intros; eapply allp_right; eauto.
Defined.
Next Obligation.
(* Goal: @derives B NB (@sepcon B NB SB (P x) (Q x)) (R x) *)
(* Goal: forall _ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho)), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
 intros; split; intros;  eapply imp_andp_adjoint; eauto.
Defined.
Next Obligation.
(* Goal: @derives B ND (@prop B ND P) (Q x) *)
 intros; eapply prop_left; eauto.
Defined.
Next Obligation.
(* Goal: @derives B ND (Q x) (@prop B ND P) *)
 intros; eapply prop_right; eauto.
Defined.
Next Obligation.
(* Goal: @derives B ND (@imp B ND (@prop B ND P) (@prop B ND Q)) (@prop B ND (forall _ : P, Q)) *)
 intros; eapply prop_imp_prop_left; eauto.
Defined.
Next Obligation.
(* Goal: @derives B ND (@allp B ND B0 (fun x : B0 => @prop B ND (P x))) (@prop B ND (forall b : B0, P b)) *)
 intros; eapply allp_prop_left; eauto.
Defined.

Delimit Scope logic with logic.
Local Open Scope logic.
Notation "P '|--' Q" := (derives P Q) (at level 80, no associativity).
Notation "'EX'  x ':' T ',' P " := (exp (fun x:T => P%logic)) (at level 65, x at level 99) : logic.
Notation "'ALL'  x ':' T  ',' P " := (allp (fun x:T => P%logic)) (at level 65, x at level 99) : logic.
Infix "||" := orp (at level 50, left associativity) : logic.
Infix "&&" := andp (at level 40, left associativity) : logic.
Notation "P '-->' Q" := (imp P Q) (at level 55, right associativity) : logic.
Notation "P '<-->' Q" := (andp (imp P Q) (imp Q P)) (at level 57, no associativity) : logic.
Notation "'!!' e" := (prop e) (at level 25) : logic.

Class SepLog (A: Type) {ND: NatDed A} := mkSepLog {
  emp: A;
  sepcon: A -> A -> A;
  wand: A -> A -> A;
  ewand: A -> A -> A;
  sepcon_assoc: forall P Q R, sepcon (sepcon P Q) R = sepcon P (sepcon Q R);
  sepcon_comm:  forall P Q, sepcon P Q = sepcon Q P;
  wand_sepcon_adjoint: forall (P Q R: A),  (sepcon P Q |-- R) <-> (P |-- wand Q R);
  sepcon_andp_prop: forall P Q R, sepcon P (!!Q && R) = !!Q && (sepcon P R);
  sepcon_derives: forall P P' Q Q' : A, P |-- P' -> Q |-- Q' -> sepcon P Q |-- sepcon P' Q';
  ewand_sepcon: forall (P Q R : A),  ewand (sepcon P Q) R = ewand P (ewand Q R);
  ewand_TT_sepcon: forall (P Q R: A),
                         andp (sepcon P Q) (ewand R TT) |--
                               sepcon (andp P (ewand R TT)) (andp Q (ewand R TT));
  exclude_elsewhere: forall P Q: A, sepcon P Q |-- sepcon (andp P (ewand Q TT)) Q;
  ewand_conflict: forall P Q R, sepcon P Q |-- FF -> andp P (ewand Q R) |-- FF
}.

Notation "P '*' Q" := (sepcon P Q) : logic.
Notation "P '-*' Q" := (wand P Q) (at level 60, right associativity) : logic.

Instance LiftSepLog (A B: Type) {NB: NatDed B}{SB: SepLog B} : SepLog (A -> B).
 apply (mkSepLog (A -> B) _ (fun rho => emp)
            (fun P Q rho => P rho * Q rho) (fun P Q rho => P rho -* Q rho)
            (fun P Q rho => ewand (P rho) (Q rho))).
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @sepcon B NB SB (P rho) (@sepcon B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (Q rho) (P rho)) *)
(* Goal: forall P Q R : forall _ : A, B, iff (@derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R) (@derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho))) *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
 (* sepcon_assoc *) intros; extensionality rho; apply sepcon_assoc.
(* Goal: forall P Q : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (Q rho) (P rho)) *)
(* Goal: forall P Q R : forall _ : A, B, iff (@derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R) (@derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho))) *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
 (* sepcon_comm *) intros; extensionality rho; apply sepcon_comm.
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
 intros.  split. simpl. intuition.
(* Goal: @derives B NB (P x) (@wand B NB SB (Q x) (R x)) *)
(* Goal: forall _ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho)), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
    apply wand_sepcon_adjoint. auto.
(* Goal: @derives B NB (@sepcon B NB SB (P x) (Q x)) (R x) *)
(* Goal: forall _ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho)), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
    intro. intro rho.     apply <- wand_sepcon_adjoint; auto.
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
 simpl; intros. extensionality x. apply sepcon_andp_prop.
(* Goal: @derives B NB (@sepcon B NB SB (P x) (Q x)) (R x) *)
(* Goal: forall _ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho)), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
 simpl; intros; apply sepcon_derives; auto.
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
 simpl; intros; extensionality x; apply ewand_sepcon.
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
 simpl; intros; eapply ewand_TT_sepcon.
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
 simpl; intros; eapply exclude_elsewhere.
(* Goal: @derives B NB (@sepcon B NB SB (P x) (Q x)) (R x) *)
(* Goal: forall _ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho)), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
 simpl; intros; eapply ewand_conflict; eauto.
Defined.

Class ClassicalSep  (A: Type) {ND: NatDed A}{SL: SepLog A} := mkCS {
   sepcon_emp: forall P, P * emp = P
}.

Instance LiftClassicalSep (A B: Type)  {NB: NatDed B}{SB: SepLog B}{CB: ClassicalSep B} :
        ClassicalSep (A -> B).
(* Goal: @ClassicalSep (forall _ : A, B) (@LiftNatDed A B NB) (@LiftSepLog A B NB SB) *)
 apply mkCS.
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
 intros. extensionality x. simpl. apply sepcon_emp.
Qed.

Definition  extensible {A}{ND: NatDed A}{SL: SepLog A}(P:A) := sepcon P TT |-- P.

Class IntuitionisticSep (A: Type) {ND: NatDed A}{SL: SepLog A} := mkIS {
   all_extensible: forall P, extensible P
}.

Instance LiftIntuitionisticSep (A B: Type)  {NB: NatDed B}{SB: SepLog B}{IB: IntuitionisticSep B} :
        IntuitionisticSep (A -> B).
(* Goal: @IntuitionisticSep (forall _ : A, B) (@LiftNatDed A B NB) (@LiftSepLog A B NB SB) *)
 apply mkIS.
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
 intros. intro. simpl. apply all_extensible.
Qed.

Class Indir (A: Type) {ND: NatDed A} := mkIndir {
  later: A -> A;
  now_later: forall P: A, P |-- later P;
  later_K: forall P Q, later (P --> Q) |-- later P --> later Q;
  later_allp: forall T (F: T -> A),  later (allp F) = ALL x:T, later (F x);
  later_exp: forall T (F: T-> A), EX x:T, later (F x) |-- later (exp F);
  later_exp': forall T (any:T) F, later (exp F) = EX x:T, later (F x);
  later_exp'': forall T F, later (exp F) |-- (EX x:T, later (F x)) || later FF;
  later_imp: forall P Q,  later(P --> Q) = later P --> later Q;
  later_prop: forall PP: Prop, later (!! PP) |-- !! PP || later FF;
  loeb: forall P,   later P |-- P ->  TT |-- P
}.

Notation "'|>' e" := (later e) (at level 30, right associativity): logic.

Instance LiftIndir (A: Type) (B: Type)  {NB: NatDed B}{IXB: Indir B} :
         @Indir (A -> B) (LiftNatDed A B).
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
 apply (mkIndir _ _ (fun P rho => later (P rho))); intros; simpl in *; intros.
(* Goal: @derives B NB (P x) (@later B NB IXB (P x)) *)
(* Goal: @derives B NB (@later B NB IXB (@imp B NB (P x) (Q x))) (@imp B NB (@later B NB IXB (P x)) (@later B NB IXB (Q x))) *)
(* Goal: @eq (forall _ : A, B) (fun rho : A => @later B NB IXB (@allp B NB T (fun x : T => F x rho))) (fun a : A => @allp B NB T (fun x : T => @later B NB IXB (F x a))) *)
(* Goal: @derives B NB (@exp B NB T (fun x0 : T => @later B NB IXB (F x0 x))) (@later B NB IXB (@exp B NB T (fun x0 : T => F x0 x))) *)
(* Goal: @eq (forall _ : A, B) (fun rho : A => @later B NB IXB (@exp B NB T (fun x : T => F x rho))) (fun a : A => @exp B NB T (fun x : T => @later B NB IXB (F x a))) *)
(* Goal: @derives B NB (@later B NB IXB (@exp B NB T (fun x0 : T => F x0 x))) (@orp B NB (@exp B NB T (fun x0 : T => @later B NB IXB (F x0 x))) (@later B NB IXB (@prop B NB False))) *)
(* Goal: @eq (forall _ : A, B) (fun rho : A => @later B NB IXB (@imp B NB (P rho) (Q rho))) (fun x : A => @imp B NB (@later B NB IXB (P x)) (@later B NB IXB (Q x))) *)
(* Goal: @derives B NB (@later B NB IXB (@prop B NB PP)) (@orp B NB (@prop B NB PP) (@later B NB IXB (@prop B NB False))) *)
(* Goal: @derives B NB (@prop B NB True) (P x) *)
 apply now_later.
(* Goal: @derives B NB (@later B NB IXB (@imp B NB (P x) (Q x))) (@imp B NB (@later B NB IXB (P x)) (@later B NB IXB (Q x))) *)
(* Goal: @eq (forall _ : A, B) (fun rho : A => @later B NB IXB (@allp B NB T (fun x : T => F x rho))) (fun a : A => @allp B NB T (fun x : T => @later B NB IXB (F x a))) *)
(* Goal: @derives B NB (@exp B NB T (fun x0 : T => @later B NB IXB (F x0 x))) (@later B NB IXB (@exp B NB T (fun x0 : T => F x0 x))) *)
(* Goal: @eq (forall _ : A, B) (fun rho : A => @later B NB IXB (@exp B NB T (fun x : T => F x rho))) (fun a : A => @exp B NB T (fun x : T => @later B NB IXB (F x a))) *)
(* Goal: @derives B NB (@later B NB IXB (@exp B NB T (fun x0 : T => F x0 x))) (@orp B NB (@exp B NB T (fun x0 : T => @later B NB IXB (F x0 x))) (@later B NB IXB (@prop B NB False))) *)
(* Goal: @eq (forall _ : A, B) (fun rho : A => @later B NB IXB (@imp B NB (P rho) (Q rho))) (fun x : A => @imp B NB (@later B NB IXB (P x)) (@later B NB IXB (Q x))) *)
(* Goal: @derives B NB (@later B NB IXB (@prop B NB PP)) (@orp B NB (@prop B NB PP) (@later B NB IXB (@prop B NB False))) *)
(* Goal: @derives B NB (@prop B NB True) (P x) *)
 apply later_K.
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
 simpl; intros. extensionality rho. apply later_allp.
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
 simpl; intros. apply later_exp.
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
 simpl; intros. extensionality rho. apply later_exp'; auto.
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
 simpl; intros. apply later_exp''.
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
 simpl; intros. extensionality rho. apply later_imp.
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
 simpl; intros. apply later_prop.
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
 simpl; intros. apply loeb; auto.
Defined.

Class SepIndir (A: Type) {NA: NatDed A}{SA: SepLog A}{IA: Indir A} := mkSepIndir {
  later_sepcon: forall P Q, |> (P * Q) = |>P * |>Q;
  later_wand: forall P Q, |> (P -* Q) = |>P -* |>Q;
  later_ewand: forall P Q, |> (ewand P Q) = ewand (|>P) (|>Q)
}.

Instance LiftSepIndir  (A: Type) (B: Type)  {NB: NatDed B} {SB: SepLog B}{IB: Indir B}{SIB: SepIndir B} :
     @SepIndir (A -> B) (LiftNatDed A B) (LiftSepLog A B) (LiftIndir A B).
(* Goal: @SepIndir (forall _ : A, B) (@LiftNatDed A B NB) (@LiftSepLog A B NB SB) (@LiftIndir A B NB IB) *)
 constructor.
(* Goal: @derives B NB (@sepcon (forall _ : A, B) (@LiftNatDed A B NB) (@LiftSepLog A B NB SB) P (@TT (forall _ : A, B) (@LiftNatDed A B NB)) x) (P x) *)
 intros; simpl. extensionality rho.  apply later_sepcon.
(* Goal: @derives B NB (@sepcon (forall _ : A, B) (@LiftNatDed A B NB) (@LiftSepLog A B NB SB) P (@TT (forall _ : A, B) (@LiftNatDed A B NB)) x) (P x) *)
 intros; simpl. extensionality rho.  apply later_wand.
(* Goal: @derives B NB (@sepcon (forall _ : A, B) (@LiftNatDed A B NB) (@LiftSepLog A B NB SB) P (@TT (forall _ : A, B) (@LiftNatDed A B NB)) x) (P x) *)
 intros; simpl. extensionality rho.  apply later_ewand.
Defined.

Class CorableSepLog (A: Type) {ND: NatDed A}{SL: SepLog A}:= mkCorableSepLog {
  corable: A -> Prop;
  corable_prop: forall P, corable (!! P);
  corable_andp: forall P Q, corable P -> corable Q -> corable (P && Q);
  corable_orp: forall P Q, corable P -> corable Q -> corable (P || Q);
  corable_imp: forall P Q, corable P -> corable Q -> corable (P --> Q);
  corable_allp: forall {B: Type} (P:  B -> A), (forall b, corable (P b)) -> corable (allp P);
  corable_exp: forall {B: Type} (P:  B -> A), (forall b, corable (P b)) -> corable (exp P);
  corable_sepcon: forall P Q, corable P -> corable Q -> corable (P * Q);
  corable_wand: forall P Q, corable P -> corable Q -> corable (P -* Q);
  corable_andp_sepcon1: forall P Q R, corable P ->  (P && Q) * R = P && (Q * R)
}.

Instance LiftCorableSepLog (A: Type) (B: Type) {NB: NatDed B} {SB: SepLog B} {CSL: CorableSepLog B} : @CorableSepLog (A -> B) (LiftNatDed A B) (LiftSepLog A B).
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
  apply (@mkCorableSepLog _ _ _ (fun P => forall b, corable (P b))); intros; simpl in *; intros.
  + apply corable_prop.
(* Goal: @derives B NB (@sepcon B NB SB (P x) (Q x)) (R x) *)
(* Goal: forall _ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho)), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
  + apply corable_andp; auto.
(* Goal: @derives B NB (@sepcon B NB SB (P x) (Q x)) (R x) *)
(* Goal: forall _ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho)), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
  + apply corable_orp; auto.
(* Goal: @derives B NB (@sepcon B NB SB (P x) (Q x)) (R x) *)
(* Goal: forall _ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho)), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
  + apply corable_imp; auto.
(* Goal: @derives B NB (@sepcon B NB SB (P x) (Q x)) (R x) *)
(* Goal: forall _ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho)), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
  + apply corable_allp; auto.
(* Goal: @derives B NB (@sepcon B NB SB (P x) (Q x)) (R x) *)
(* Goal: forall _ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho)), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
  + apply corable_exp; auto.
(* Goal: @derives B NB (@sepcon B NB SB (P x) (Q x)) (R x) *)
(* Goal: forall _ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho)), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
  + apply corable_sepcon; auto.
(* Goal: @derives B NB (@sepcon B NB SB (P x) (Q x)) (R x) *)
(* Goal: forall _ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho)), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
  + apply corable_wand; auto.
  + extensionality b.
(* Goal: @derives B NB (@sepcon B NB SB (P x) (Q x)) (R x) *)
(* Goal: forall _ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho)), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
    apply corable_andp_sepcon1; auto.
Defined.

Class CorableIndir (A: Type) {ND: NatDed A}{SL: SepLog A}{CSL: CorableSepLog A}{ID: Indir A} :=
  corable_later: forall P, corable P -> corable (|> P).

Instance LiftCorableIndir (A: Type) (B: Type) {NB: NatDed B} {SB: SepLog B} {CSL: CorableSepLog B} {ID: Indir B} {CI: CorableIndir B}: @CorableIndir (A -> B) (LiftNatDed A B) (LiftSepLog A B) (LiftCorableSepLog A B) (LiftIndir A B).
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
  unfold CorableIndir; simpl; intros.
(* Goal: @derives B NB (@sepcon B NB SB (P x) (Q x)) (R x) *)
(* Goal: forall _ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @wand B NB SB (Q rho) (R rho)), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) R *)
(* Goal: forall (P : forall _ : A, B) (Q : Prop) (R : forall _ : A, B), @eq (forall _ : A, B) (fun rho : A => @sepcon B NB SB (P rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) R rho)) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (@prop (forall _ : A, B) (@LiftNatDed A B NB) Q) (fun rho : A => @sepcon B NB SB (P rho) (R rho))) *)
(* Goal: forall (P P' Q Q' : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) P P') (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) Q Q'), @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (P' rho) (Q' rho)) *)
(* Goal: forall P Q R : forall _ : A, B, @eq (forall _ : A, B) (fun rho : A => @ewand B NB SB (@sepcon B NB SB (P rho) (Q rho)) (R rho)) (fun rho : A => @ewand B NB SB (P rho) (@ewand B NB SB (Q rho) (R rho))) *)
(* Goal: forall P Q R : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @ewand B NB SB (R rho) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho))) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (@andp (forall _ : A, B) (@LiftNatDed A B NB) Q (fun rho0 : A => @ewand B NB SB (R rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho)) *)
(* Goal: forall P Q : forall _ : A, B, @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (fun rho : A => @sepcon B NB SB (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho0 : A => @ewand B NB SB (Q rho0) (@TT (forall _ : A, B) (@LiftNatDed A B NB) rho0)) rho) (Q rho)) *)
(* Goal: forall (P Q R : forall _ : A, B) (_ : @derives (forall _ : A, B) (@LiftNatDed A B NB) (fun rho : A => @sepcon B NB SB (P rho) (Q rho)) (@FF (forall _ : A, B) (@LiftNatDed A B NB))), @derives (forall _ : A, B) (@LiftNatDed A B NB) (@andp (forall _ : A, B) (@LiftNatDed A B NB) P (fun rho : A => @ewand B NB SB (Q rho) (R rho))) (@FF (forall _ : A, B) (@LiftNatDed A B NB)) *)
  apply corable_later; auto.
Defined.

Lemma orp_comm: forall {A: Type} `{NatDed A} (P Q: A), P || Q = Q || P.
Proof.
(* Goal: forall (A : Type) (H : NatDed A) (P Q : A), @eq A (@orp A H P Q) (@orp A H Q P) *)
  intros.
(* Goal: @eq A (@orp A H P Q) (@orp A H Q P) *)
  apply pred_ext.
  + apply orp_left; [apply orp_right2 | apply orp_right1]; apply derives_refl.
  + apply orp_left; [apply orp_right2 | apply orp_right1]; apply derives_refl.
Qed.

