Require Import VST.msl.seplog.
Require Import VST.msl.base.
Require Import VST.msl.ageable.
Require Import VST.msl.sepalg.
Require Import VST.msl.age_sepalg.
Require Import VST.msl.predicates_hered.
Require Import VST.msl.predicates_sl.
Require Import VST.msl.subtypes.
Require Import VST.msl.subtypes_sl.
Require Import VST.msl.predicates_rec.
Require Import VST.msl.contractive.
Require VST.msl.normalize.

Local Open Scope logic.

Instance algNatDed (T: Type){agT: ageable T} : NatDed (pred T).
  apply (mkNatDed _
                    predicates_hered.andp
                    predicates_hered.orp
                    (@predicates_hered.exp _ _)
                    (@predicates_hered.allp _ _)
                    predicates_hered.imp predicates_hered.prop
                    (@predicates_hered.derives _ _)).
(* Goal: forall (P Q : @pred T agT) (_ : @derives T agT P Q) (_ : @derives T agT Q P), @eq (@pred T agT) P Q *)
(* Goal: forall P : @pred T agT, @derives T agT P P *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P Q) (_ : @derives T agT Q R), @derives T agT P R *)
(* Goal: forall (X P Q : @pred T agT) (_ : @derives T agT X P) (_ : @derives T agT X Q), @derives T agT X (@andp T agT P Q) *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R), @derives T agT (@andp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT Q R), @derives T agT (@andp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R) (_ : @derives T agT Q R), @derives T agT (@orp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P Q), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (B : Type) (x : B) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : @derives T agT P (Q x)), @derives T agT P (@exp T agT B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (Q : @pred T agT) (_ : forall x : B, @derives T agT (P x) Q), @derives T agT (@exp T agT B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (x : B) (Q : @pred T agT) (_ : @derives T agT (P x) Q), @derives T agT (@allp T agT B P) Q *)
(* Goal: forall (B : Type) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : forall v : B, @derives T agT P (Q v)), @derives T agT P (@allp T agT B Q) *)
(* Goal: forall P Q R : @pred T agT, iff (@derives T agT (@andp T agT P Q) R) (@derives T agT P (@imp T agT Q R)) *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : forall _ : P, @derives T agT (@prop T agT True) Q), @derives T agT (@prop T agT P) Q *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : P), @derives T agT Q (@prop T agT P) *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 apply pred_ext.
(* Goal: forall P : @pred T agT, @derives T agT P P *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P Q) (_ : @derives T agT Q R), @derives T agT P R *)
(* Goal: forall (X P Q : @pred T agT) (_ : @derives T agT X P) (_ : @derives T agT X Q), @derives T agT X (@andp T agT P Q) *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R), @derives T agT (@andp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT Q R), @derives T agT (@andp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R) (_ : @derives T agT Q R), @derives T agT (@orp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P Q), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (B : Type) (x : B) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : @derives T agT P (Q x)), @derives T agT P (@exp T agT B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (Q : @pred T agT) (_ : forall x : B, @derives T agT (P x) Q), @derives T agT (@exp T agT B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (x : B) (Q : @pred T agT) (_ : @derives T agT (P x) Q), @derives T agT (@allp T agT B P) Q *)
(* Goal: forall (B : Type) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : forall v : B, @derives T agT P (Q v)), @derives T agT P (@allp T agT B Q) *)
(* Goal: forall P Q R : @pred T agT, iff (@derives T agT (@andp T agT P Q) R) (@derives T agT P (@imp T agT Q R)) *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : forall _ : P, @derives T agT (@prop T agT True) Q), @derives T agT (@prop T agT P) Q *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : P), @derives T agT Q (@prop T agT P) *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 apply derives_refl.
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P Q) (_ : @derives T agT Q R), @derives T agT P R *)
(* Goal: forall (X P Q : @pred T agT) (_ : @derives T agT X P) (_ : @derives T agT X Q), @derives T agT X (@andp T agT P Q) *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R), @derives T agT (@andp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT Q R), @derives T agT (@andp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R) (_ : @derives T agT Q R), @derives T agT (@orp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P Q), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (B : Type) (x : B) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : @derives T agT P (Q x)), @derives T agT P (@exp T agT B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (Q : @pred T agT) (_ : forall x : B, @derives T agT (P x) Q), @derives T agT (@exp T agT B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (x : B) (Q : @pred T agT) (_ : @derives T agT (P x) Q), @derives T agT (@allp T agT B P) Q *)
(* Goal: forall (B : Type) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : forall v : B, @derives T agT P (Q v)), @derives T agT P (@allp T agT B Q) *)
(* Goal: forall P Q R : @pred T agT, iff (@derives T agT (@andp T agT P Q) R) (@derives T agT P (@imp T agT Q R)) *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : forall _ : P, @derives T agT (@prop T agT True) Q), @derives T agT (@prop T agT P) Q *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : P), @derives T agT Q (@prop T agT P) *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 apply derives_trans.
(* Goal: forall (X P Q : @pred T agT) (_ : @derives T agT X P) (_ : @derives T agT X Q), @derives T agT X (@andp T agT P Q) *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R), @derives T agT (@andp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT Q R), @derives T agT (@andp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R) (_ : @derives T agT Q R), @derives T agT (@orp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P Q), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (B : Type) (x : B) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : @derives T agT P (Q x)), @derives T agT P (@exp T agT B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (Q : @pred T agT) (_ : forall x : B, @derives T agT (P x) Q), @derives T agT (@exp T agT B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (x : B) (Q : @pred T agT) (_ : @derives T agT (P x) Q), @derives T agT (@allp T agT B P) Q *)
(* Goal: forall (B : Type) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : forall v : B, @derives T agT P (Q v)), @derives T agT P (@allp T agT B Q) *)
(* Goal: forall P Q R : @pred T agT, iff (@derives T agT (@andp T agT P Q) R) (@derives T agT P (@imp T agT Q R)) *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : forall _ : P, @derives T agT (@prop T agT True) Q), @derives T agT (@prop T agT P) Q *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : P), @derives T agT Q (@prop T agT P) *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 apply andp_right.
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R), @derives T agT (@andp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT Q R), @derives T agT (@andp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R) (_ : @derives T agT Q R), @derives T agT (@orp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P Q), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (B : Type) (x : B) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : @derives T agT P (Q x)), @derives T agT P (@exp T agT B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (Q : @pred T agT) (_ : forall x : B, @derives T agT (P x) Q), @derives T agT (@exp T agT B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (x : B) (Q : @pred T agT) (_ : @derives T agT (P x) Q), @derives T agT (@allp T agT B P) Q *)
(* Goal: forall (B : Type) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : forall v : B, @derives T agT P (Q v)), @derives T agT P (@allp T agT B Q) *)
(* Goal: forall P Q R : @pred T agT, iff (@derives T agT (@andp T agT P Q) R) (@derives T agT P (@imp T agT Q R)) *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : forall _ : P, @derives T agT (@prop T agT True) Q), @derives T agT (@prop T agT P) Q *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : P), @derives T agT Q (@prop T agT P) *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 apply andp_left1.
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT Q R), @derives T agT (@andp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R) (_ : @derives T agT Q R), @derives T agT (@orp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P Q), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (B : Type) (x : B) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : @derives T agT P (Q x)), @derives T agT P (@exp T agT B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (Q : @pred T agT) (_ : forall x : B, @derives T agT (P x) Q), @derives T agT (@exp T agT B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (x : B) (Q : @pred T agT) (_ : @derives T agT (P x) Q), @derives T agT (@allp T agT B P) Q *)
(* Goal: forall (B : Type) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : forall v : B, @derives T agT P (Q v)), @derives T agT P (@allp T agT B Q) *)
(* Goal: forall P Q R : @pred T agT, iff (@derives T agT (@andp T agT P Q) R) (@derives T agT P (@imp T agT Q R)) *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : forall _ : P, @derives T agT (@prop T agT True) Q), @derives T agT (@prop T agT P) Q *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : P), @derives T agT Q (@prop T agT P) *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 apply andp_left2.
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R) (_ : @derives T agT Q R), @derives T agT (@orp T agT P Q) R *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P Q), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (B : Type) (x : B) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : @derives T agT P (Q x)), @derives T agT P (@exp T agT B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (Q : @pred T agT) (_ : forall x : B, @derives T agT (P x) Q), @derives T agT (@exp T agT B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (x : B) (Q : @pred T agT) (_ : @derives T agT (P x) Q), @derives T agT (@allp T agT B P) Q *)
(* Goal: forall (B : Type) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : forall v : B, @derives T agT P (Q v)), @derives T agT P (@allp T agT B Q) *)
(* Goal: forall P Q R : @pred T agT, iff (@derives T agT (@andp T agT P Q) R) (@derives T agT P (@imp T agT Q R)) *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : forall _ : P, @derives T agT (@prop T agT True) Q), @derives T agT (@prop T agT P) Q *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : P), @derives T agT Q (@prop T agT P) *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 apply orp_left.
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P Q), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (B : Type) (x : B) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : @derives T agT P (Q x)), @derives T agT P (@exp T agT B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (Q : @pred T agT) (_ : forall x : B, @derives T agT (P x) Q), @derives T agT (@exp T agT B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (x : B) (Q : @pred T agT) (_ : @derives T agT (P x) Q), @derives T agT (@allp T agT B P) Q *)
(* Goal: forall (B : Type) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : forall v : B, @derives T agT P (Q v)), @derives T agT P (@allp T agT B Q) *)
(* Goal: forall P Q R : @pred T agT, iff (@derives T agT (@andp T agT P Q) R) (@derives T agT P (@imp T agT Q R)) *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : forall _ : P, @derives T agT (@prop T agT True) Q), @derives T agT (@prop T agT P) Q *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : P), @derives T agT Q (@prop T agT P) *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 apply orp_right1.
(* Goal: forall (P Q R : @pred T agT) (_ : @derives T agT P R), @derives T agT P (@orp T agT Q R) *)
(* Goal: forall (B : Type) (x : B) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : @derives T agT P (Q x)), @derives T agT P (@exp T agT B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (Q : @pred T agT) (_ : forall x : B, @derives T agT (P x) Q), @derives T agT (@exp T agT B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (x : B) (Q : @pred T agT) (_ : @derives T agT (P x) Q), @derives T agT (@allp T agT B P) Q *)
(* Goal: forall (B : Type) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : forall v : B, @derives T agT P (Q v)), @derives T agT P (@allp T agT B Q) *)
(* Goal: forall P Q R : @pred T agT, iff (@derives T agT (@andp T agT P Q) R) (@derives T agT P (@imp T agT Q R)) *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : forall _ : P, @derives T agT (@prop T agT True) Q), @derives T agT (@prop T agT P) Q *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : P), @derives T agT Q (@prop T agT P) *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 apply orp_right2.
(* Goal: forall (B : Type) (x : B) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : @derives T agT P (Q x)), @derives T agT P (@exp T agT B Q) *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (Q : @pred T agT) (_ : forall x : B, @derives T agT (P x) Q), @derives T agT (@exp T agT B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (x : B) (Q : @pred T agT) (_ : @derives T agT (P x) Q), @derives T agT (@allp T agT B P) Q *)
(* Goal: forall (B : Type) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : forall v : B, @derives T agT P (Q v)), @derives T agT P (@allp T agT B Q) *)
(* Goal: forall P Q R : @pred T agT, iff (@derives T agT (@andp T agT P Q) R) (@derives T agT P (@imp T agT Q R)) *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : forall _ : P, @derives T agT (@prop T agT True) Q), @derives T agT (@prop T agT P) Q *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : P), @derives T agT Q (@prop T agT P) *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 intros ? ?; apply @exp_right.
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (Q : @pred T agT) (_ : forall x : B, @derives T agT (P x) Q), @derives T agT (@exp T agT B P) Q *)
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (x : B) (Q : @pred T agT) (_ : @derives T agT (P x) Q), @derives T agT (@allp T agT B P) Q *)
(* Goal: forall (B : Type) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : forall v : B, @derives T agT P (Q v)), @derives T agT P (@allp T agT B Q) *)
(* Goal: forall P Q R : @pred T agT, iff (@derives T agT (@andp T agT P Q) R) (@derives T agT P (@imp T agT Q R)) *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : forall _ : P, @derives T agT (@prop T agT True) Q), @derives T agT (@prop T agT P) Q *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : P), @derives T agT Q (@prop T agT P) *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 intros ? ?; apply @exp_left.
(* Goal: forall (B : Type) (P : forall _ : B, @pred T agT) (x : B) (Q : @pred T agT) (_ : @derives T agT (P x) Q), @derives T agT (@allp T agT B P) Q *)
(* Goal: forall (B : Type) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : forall v : B, @derives T agT P (Q v)), @derives T agT P (@allp T agT B Q) *)
(* Goal: forall P Q R : @pred T agT, iff (@derives T agT (@andp T agT P Q) R) (@derives T agT P (@imp T agT Q R)) *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : forall _ : P, @derives T agT (@prop T agT True) Q), @derives T agT (@prop T agT P) Q *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : P), @derives T agT Q (@prop T agT P) *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 intros ? ?; apply @allp_left.
(* Goal: forall (B : Type) (P : @pred T agT) (Q : forall _ : B, @pred T agT) (_ : forall v : B, @derives T agT P (Q v)), @derives T agT P (@allp T agT B Q) *)
(* Goal: forall P Q R : @pred T agT, iff (@derives T agT (@andp T agT P Q) R) (@derives T agT P (@imp T agT Q R)) *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : forall _ : P, @derives T agT (@prop T agT True) Q), @derives T agT (@prop T agT P) Q *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : P), @derives T agT Q (@prop T agT P) *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 intros ? ?; apply @allp_right.
(* Goal: forall P Q R : @pred T agT, iff (@derives T agT (@andp T agT P Q) R) (@derives T agT P (@imp T agT Q R)) *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : forall _ : P, @derives T agT (@prop T agT True) Q), @derives T agT (@prop T agT P) Q *)
(* Goal: forall (P : Prop) (Q : @pred T agT) (_ : P), @derives T agT Q (@prop T agT P) *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 apply imp_andp_adjoint.
(* Goal: @derives T agT (@subtypes.unfash T agT (@subtypes.fash T agT P)) P *)
(* Goal: @derives nat ag_nat (@subtypes.fash T agT (@imp T agT P Q)) (@imp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @derives nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q) *)
(* Goal: @derives T agT (@subtypes.unfash T agT P) (@subtypes.unfash T agT Q) *)
(* Goal: @eq Triv (@box nat ag_nat (@laterM nat ag_nat) (@subtypes.fash T agT P)) (@subtypes.fash T agT (@box T agT (@laterM T agT) P)) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@subtypes.unfash T agT P)) (@subtypes.unfash T agT (@box nat ag_nat (@laterM nat ag_nat) P)) *)
(* Goal: @eq Triv (@subtypes.fash T agT (@andp T agT P Q)) (@andp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @eq (@pred T agT) (@subtypes.unfash T agT (@allp nat ag_nat B P)) (@allp T agT B (fun x : B => @subtypes.unfash T agT (P x))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@allp T agT B X) (@allp T agT B Y))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@exp T agT B X) (@exp T agT B Y))) *)
(* Goal: @derives T agT P Q *)
(* Goal: @derives nat ag_nat P (@subtypes.fash T agT (@imp T agT Q R)) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@prop T agT True)) *)
(* Goal: @eq (forall _ : X, @pred T agT) (@HoRec.HORec T agT X f) (f (@HoRec.HORec T agT X f)) *)
 repeat intro. eapply H; eauto. hnf; auto.
(* Goal: @derives T agT (@subtypes.unfash T agT (@subtypes.fash T agT P)) P *)
(* Goal: @derives nat ag_nat (@subtypes.fash T agT (@imp T agT P Q)) (@imp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @derives nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q) *)
(* Goal: @derives T agT (@subtypes.unfash T agT P) (@subtypes.unfash T agT Q) *)
(* Goal: @eq Triv (@box nat ag_nat (@laterM nat ag_nat) (@subtypes.fash T agT P)) (@subtypes.fash T agT (@box T agT (@laterM T agT) P)) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@subtypes.unfash T agT P)) (@subtypes.unfash T agT (@box nat ag_nat (@laterM nat ag_nat) P)) *)
(* Goal: @eq Triv (@subtypes.fash T agT (@andp T agT P Q)) (@andp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @eq (@pred T agT) (@subtypes.unfash T agT (@allp nat ag_nat B P)) (@allp T agT B (fun x : B => @subtypes.unfash T agT (P x))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@allp T agT B X) (@allp T agT B Y))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@exp T agT B X) (@exp T agT B Y))) *)
(* Goal: @derives T agT P Q *)
(* Goal: @derives nat ag_nat P (@subtypes.fash T agT (@imp T agT Q R)) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@prop T agT True)) *)
(* Goal: @eq (forall _ : X, @pred T agT) (@HoRec.HORec T agT X f) (f (@HoRec.HORec T agT X f)) *)
 repeat intro. hnf; auto.
(* Goal: @derives T agT (@subtypes.unfash T agT (@subtypes.fash T agT P)) P *)
(* Goal: @derives nat ag_nat (@subtypes.fash T agT (@imp T agT P Q)) (@imp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @derives nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q) *)
(* Goal: @derives T agT (@subtypes.unfash T agT P) (@subtypes.unfash T agT Q) *)
(* Goal: @eq Triv (@box nat ag_nat (@laterM nat ag_nat) (@subtypes.fash T agT P)) (@subtypes.fash T agT (@box T agT (@laterM T agT) P)) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@subtypes.unfash T agT P)) (@subtypes.unfash T agT (@box nat ag_nat (@laterM nat ag_nat) P)) *)
(* Goal: @eq Triv (@subtypes.fash T agT (@andp T agT P Q)) (@andp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @eq (@pred T agT) (@subtypes.unfash T agT (@allp nat ag_nat B P)) (@allp T agT B (fun x : B => @subtypes.unfash T agT (P x))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@allp T agT B X) (@allp T agT B Y))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@exp T agT B X) (@exp T agT B Y))) *)
(* Goal: @derives T agT P Q *)
(* Goal: @derives nat ag_nat P (@subtypes.fash T agT (@imp T agT Q R)) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@prop T agT True)) *)
(* Goal: @eq (forall _ : X, @pred T agT) (@HoRec.HORec T agT X f) (f (@HoRec.HORec T agT X f)) *)
 repeat intro. specialize (H a (necR_refl _)). simpl in H. auto.
(* Goal: @derives T agT (@subtypes.unfash T agT (@subtypes.fash T agT P)) P *)
(* Goal: @derives nat ag_nat (@subtypes.fash T agT (@imp T agT P Q)) (@imp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @derives nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q) *)
(* Goal: @derives T agT (@subtypes.unfash T agT P) (@subtypes.unfash T agT Q) *)
(* Goal: @eq Triv (@box nat ag_nat (@laterM nat ag_nat) (@subtypes.fash T agT P)) (@subtypes.fash T agT (@box T agT (@laterM T agT) P)) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@subtypes.unfash T agT P)) (@subtypes.unfash T agT (@box nat ag_nat (@laterM nat ag_nat) P)) *)
(* Goal: @eq Triv (@subtypes.fash T agT (@andp T agT P Q)) (@andp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @eq (@pred T agT) (@subtypes.unfash T agT (@allp nat ag_nat B P)) (@allp T agT B (fun x : B => @subtypes.unfash T agT (P x))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@allp T agT B X) (@allp T agT B Y))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@exp T agT B X) (@exp T agT B Y))) *)
(* Goal: @derives T agT P Q *)
(* Goal: @derives nat ag_nat P (@subtypes.fash T agT (@imp T agT Q R)) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@prop T agT True)) *)
(* Goal: @eq (forall _ : X, @pred T agT) (@HoRec.HORec T agT X f) (f (@HoRec.HORec T agT X f)) *)
 repeat intro. specialize (H b). simpl in H. auto.
Defined.

Instance algSepLog (T: Type) {agT: ageable T}{JoinT: Join T}{PermT: Perm_alg T}{SepT: Sep_alg T}{AgeT: Age_alg T} :
      @SepLog (pred T) (algNatDed T).
 apply (mkSepLog _ (algNatDed T) predicates_sl.emp predicates_sl.sepcon
            predicates_sl.wand predicates_sl.ewand).
(* Goal: forall P Q R : @pred T agT, @eq (@pred T agT) (@sepcon T JoinT PermT agT AgeT (@sepcon T JoinT PermT agT AgeT P Q) R) (@sepcon T JoinT PermT agT AgeT P (@sepcon T JoinT PermT agT AgeT Q R)) *)
(* Goal: forall P Q : @pred T agT, @eq (@pred T agT) (@sepcon T JoinT PermT agT AgeT P Q) (@sepcon T JoinT PermT agT AgeT Q P) *)
(* Goal: forall P Q R : @pred T agT, iff (@seplog.derives (@pred T agT) (@algNatDed T agT) (@sepcon T JoinT PermT agT AgeT P Q) R) (@seplog.derives (@pred T agT) (@algNatDed T agT) P (@wand T JoinT PermT agT AgeT Q R)) *)
(* Goal: forall (P : @pred T agT) (Q : Prop) (R : @pred T agT), @eq (@pred T agT) (@sepcon T JoinT PermT agT AgeT P (@seplog.andp (@pred T agT) (@algNatDed T agT) (@seplog.prop (@pred T agT) (@algNatDed T agT) Q) R)) (@seplog.andp (@pred T agT) (@algNatDed T agT) (@seplog.prop (@pred T agT) (@algNatDed T agT) Q) (@sepcon T JoinT PermT agT AgeT P R)) *)
(* Goal: forall (P P' Q Q' : @pred T agT) (_ : @seplog.derives (@pred T agT) (@algNatDed T agT) P P') (_ : @seplog.derives (@pred T agT) (@algNatDed T agT) Q Q'), @seplog.derives (@pred T agT) (@algNatDed T agT) (@sepcon T JoinT PermT agT AgeT P Q) (@sepcon T JoinT PermT agT AgeT P' Q') *)
(* Goal: forall P Q R : @pred T agT, @eq (@pred T agT) (@ewand T JoinT PermT agT AgeT (@sepcon T JoinT PermT agT AgeT P Q) R) (@ewand T JoinT PermT agT AgeT P (@ewand T JoinT PermT agT AgeT Q R)) *)
(* Goal: forall P Q R : @pred T agT, @seplog.derives (@pred T agT) (@algNatDed T agT) (@seplog.andp (@pred T agT) (@algNatDed T agT) (@sepcon T JoinT PermT agT AgeT P Q) (@ewand T JoinT PermT agT AgeT R (@seplog.TT (@pred T agT) (@algNatDed T agT)))) (@sepcon T JoinT PermT agT AgeT (@seplog.andp (@pred T agT) (@algNatDed T agT) P (@ewand T JoinT PermT agT AgeT R (@seplog.TT (@pred T agT) (@algNatDed T agT)))) (@seplog.andp (@pred T agT) (@algNatDed T agT) Q (@ewand T JoinT PermT agT AgeT R (@seplog.TT (@pred T agT) (@algNatDed T agT))))) *)
(* Goal: forall P Q : @pred T agT, @seplog.derives (@pred T agT) (@algNatDed T agT) (@sepcon T JoinT PermT agT AgeT P Q) (@sepcon T JoinT PermT agT AgeT (@seplog.andp (@pred T agT) (@algNatDed T agT) P (@ewand T JoinT PermT agT AgeT Q (@seplog.TT (@pred T agT) (@algNatDed T agT)))) Q) *)
(* Goal: forall (P Q R : @pred T agT) (_ : @seplog.derives (@pred T agT) (@algNatDed T agT) (@sepcon T JoinT PermT agT AgeT P Q) (@seplog.FF (@pred T agT) (@algNatDed T agT))), @seplog.derives (@pred T agT) (@algNatDed T agT) (@seplog.andp (@pred T agT) (@algNatDed T agT) P (@ewand T JoinT PermT agT AgeT Q R)) (@seplog.FF (@pred T agT) (@algNatDed T agT)) *)
 apply sepcon_assoc.
(* Goal: forall P Q : @pred T agT, @eq (@pred T agT) (@sepcon T JoinT PermT agT AgeT P Q) (@sepcon T JoinT PermT agT AgeT Q P) *)
(* Goal: forall P Q R : @pred T agT, iff (@seplog.derives (@pred T agT) (@algNatDed T agT) (@sepcon T JoinT PermT agT AgeT P Q) R) (@seplog.derives (@pred T agT) (@algNatDed T agT) P (@wand T JoinT PermT agT AgeT Q R)) *)
(* Goal: forall (P : @pred T agT) (Q : Prop) (R : @pred T agT), @eq (@pred T agT) (@sepcon T JoinT PermT agT AgeT P (@seplog.andp (@pred T agT) (@algNatDed T agT) (@seplog.prop (@pred T agT) (@algNatDed T agT) Q) R)) (@seplog.andp (@pred T agT) (@algNatDed T agT) (@seplog.prop (@pred T agT) (@algNatDed T agT) Q) (@sepcon T JoinT PermT agT AgeT P R)) *)
(* Goal: forall (P P' Q Q' : @pred T agT) (_ : @seplog.derives (@pred T agT) (@algNatDed T agT) P P') (_ : @seplog.derives (@pred T agT) (@algNatDed T agT) Q Q'), @seplog.derives (@pred T agT) (@algNatDed T agT) (@sepcon T JoinT PermT agT AgeT P Q) (@sepcon T JoinT PermT agT AgeT P' Q') *)
(* Goal: forall P Q R : @pred T agT, @eq (@pred T agT) (@ewand T JoinT PermT agT AgeT (@sepcon T JoinT PermT agT AgeT P Q) R) (@ewand T JoinT PermT agT AgeT P (@ewand T JoinT PermT agT AgeT Q R)) *)
(* Goal: forall P Q R : @pred T agT, @seplog.derives (@pred T agT) (@algNatDed T agT) (@seplog.andp (@pred T agT) (@algNatDed T agT) (@sepcon T JoinT PermT agT AgeT P Q) (@ewand T JoinT PermT agT AgeT R (@seplog.TT (@pred T agT) (@algNatDed T agT)))) (@sepcon T JoinT PermT agT AgeT (@seplog.andp (@pred T agT) (@algNatDed T agT) P (@ewand T JoinT PermT agT AgeT R (@seplog.TT (@pred T agT) (@algNatDed T agT)))) (@seplog.andp (@pred T agT) (@algNatDed T agT) Q (@ewand T JoinT PermT agT AgeT R (@seplog.TT (@pred T agT) (@algNatDed T agT))))) *)
(* Goal: forall P Q : @pred T agT, @seplog.derives (@pred T agT) (@algNatDed T agT) (@sepcon T JoinT PermT agT AgeT P Q) (@sepcon T JoinT PermT agT AgeT (@seplog.andp (@pred T agT) (@algNatDed T agT) P (@ewand T JoinT PermT agT AgeT Q (@seplog.TT (@pred T agT) (@algNatDed T agT)))) Q) *)
(* Goal: forall (P Q R : @pred T agT) (_ : @seplog.derives (@pred T agT) (@algNatDed T agT) (@sepcon T JoinT PermT agT AgeT P Q) (@seplog.FF (@pred T agT) (@algNatDed T agT))), @seplog.derives (@pred T agT) (@algNatDed T agT) (@seplog.andp (@pred T agT) (@algNatDed T agT) P (@ewand T JoinT PermT agT AgeT Q R)) (@seplog.FF (@pred T agT) (@algNatDed T agT)) *)
 apply sepcon_comm.
(* Goal: le y a *)
 intros. pose proof (wand_sepcon_adjoint P Q R). simpl. rewrite H; split; auto.
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@exp T agT T0 F)) (@orp T agT (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@imp T agT P Q)) (@imp T agT (@box T agT (@laterM T agT) P) (@box T agT (@laterM T agT) Q)) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@prop T agT PP)) (@orp T agT (@prop T agT PP) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @derives T agT (@prop T agT True) P *)
 intros; simpl. apply predicates_hered.pred_ext; simpl.
(* Goal: le y a *)
          intros ? [w1 [w2 [? [? [? ?]]]]];  split; auto. exists w1; exists w2; repeat split; auto.
(* Goal: le y a *)
          intros ? [? [w1 [w2 [? [? ?]]]]];  exists w1; exists w2; repeat split; auto.
(* Goal: le y a *)
 intros; intro; apply sepcon_derives; auto.
(* Goal: le y a *)
 intros; simpl; apply ewand_sepcon; auto.
(* Goal: le y a *)
 intros; simpl. apply ewand_TT_sepcon; auto.
(* Goal: le y a *)
 intros; simpl. intros w [w1 [w2 [? [? ?]]]]. exists w1,w2; repeat split; auto. exists w2; exists w; repeat split; auto.
(* Goal: le y a *)
  intros; simpl. apply ewand_conflict; auto.
Defined.

Instance algClassicalSep (T: Type) {agT: ageable T}{JoinT: Join T}{PermT: Perm_alg T}{SepT: Sep_alg T}{AgeT: Age_alg T}:
     @ClassicalSep (pred T) (algNatDed T)(algSepLog T).
(* Goal: forall P : Triv, @eq Triv (@fash Triv TrivNatDed TrivIndir TrivRecIndir P) P *)
 constructor; intros. simpl. apply predicates_sl.sepcon_emp.
Qed.

Definition Triv := predicates_hered.pred nat.
Instance TrivNatDed: NatDed Triv := algNatDed nat.
Instance TrivSeplog: SepLog Triv := @algSepLog nat _ _ _ _ (asa_nat).
Instance TrivClassical: ClassicalSep Triv := @algClassicalSep _ _ _ _ _ asa_nat.
Instance TrivIntuitionistic: IntuitionisticSep Triv.
(* Goal: forall P : Triv, @eq Triv (@fash Triv TrivNatDed TrivIndir TrivRecIndir P) P *)
 constructor. intros. hnf. intros. destruct H as [w1 [w2 [? [? _]]]].
(* Goal: le y a *)
 destruct H; subst; auto.
Qed.

Instance algIndir (T: Type) {agT: ageable T}{JoinT: Join T}{PermT: Perm_alg T}{SepT: Sep_alg T}
                {AgeT: Age_alg T}:
         @Indir (pred T) (algNatDed T).
(* Goal: @Indir (@pred T agT) (@algNatDed T agT) *)
 apply (mkIndir _ _ (box laterM)); intros; simpl in *.
(* Goal: @derives T agT P (@box T agT (@laterM T agT) P) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@imp T agT P Q)) (@imp T agT (@box T agT (@laterM T agT) P) (@box T agT (@laterM T agT) Q)) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@allp T agT T0 F)) (@allp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) *)
(* Goal: @derives T agT (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) (@box T agT (@laterM T agT) (@exp T agT T0 F)) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@exp T agT T0 F)) (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@exp T agT T0 F)) (@orp T agT (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@imp T agT P Q)) (@imp T agT (@box T agT (@laterM T agT) P) (@box T agT (@laterM T agT) Q)) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@prop T agT PP)) (@orp T agT (@prop T agT PP) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @derives T agT (@prop T agT True) P *)
 apply @predicates_hered.now_later.
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@imp T agT P Q)) (@imp T agT (@box T agT (@laterM T agT) P) (@box T agT (@laterM T agT) Q)) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@allp T agT T0 F)) (@allp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) *)
(* Goal: @derives T agT (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) (@box T agT (@laterM T agT) (@exp T agT T0 F)) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@exp T agT T0 F)) (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@exp T agT T0 F)) (@orp T agT (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@imp T agT P Q)) (@imp T agT (@box T agT (@laterM T agT) P) (@box T agT (@laterM T agT) Q)) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@prop T agT PP)) (@orp T agT (@prop T agT PP) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @derives T agT (@prop T agT True) P *)
 apply @predicates_hered.axiomK.
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@allp T agT T0 F)) (@allp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) *)
(* Goal: @derives T agT (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) (@box T agT (@laterM T agT) (@exp T agT T0 F)) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@exp T agT T0 F)) (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@exp T agT T0 F)) (@orp T agT (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@imp T agT P Q)) (@imp T agT (@box T agT (@laterM T agT) P) (@box T agT (@laterM T agT) Q)) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@prop T agT PP)) (@orp T agT (@prop T agT PP) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @derives T agT (@prop T agT True) P *)
 apply @predicates_hered.later_allp.
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@exp T agT T0 F)) (@orp T agT (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@imp T agT P Q)) (@imp T agT (@box T agT (@laterM T agT) P) (@box T agT (@laterM T agT) Q)) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@prop T agT PP)) (@orp T agT (@prop T agT PP) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @derives T agT (@prop T agT True) P *)
 simpl. intros; apply @box_ex.
(* Goal: le y a *)
 simpl. intros; apply @later_ex; auto.
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@exp T agT T0 F)) (@orp T agT (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@imp T agT P Q)) (@imp T agT (@box T agT (@laterM T agT) P) (@box T agT (@laterM T agT) Q)) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@prop T agT PP)) (@orp T agT (@prop T agT PP) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @derives T agT (@prop T agT True) P *)
 simpl. intros; apply @later_ex''.
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@imp T agT P Q)) (@imp T agT (@box T agT (@laterM T agT) P) (@box T agT (@laterM T agT) Q)) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@prop T agT PP)) (@orp T agT (@prop T agT PP) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @derives T agT (@prop T agT True) P *)
 apply @predicates_hered.later_imp.
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@prop T agT PP)) (@orp T agT (@prop T agT PP) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @derives T agT (@prop T agT True) P *)
 apply @predicates_hered.later_prop.
(* Goal: le y a *)
 apply @predicates_hered.loeb; auto.
Defined.

Instance TrivIndir: Indir Triv := @algIndir nat _ _ _ _ asa_nat.

Section SL2. Import VST.msl.seplog.

Class RecIndir (A: Type) {NA: NatDed A}{IA: Indir A} := mkRecIndir {
  fash : A -> Triv;
  unfash : Triv -> A;
  HORec : forall {X} (f: (X -> A) -> (X -> A)), X -> A;
  unfash_fash:  forall P: A, unfash (fash P) |-- P;
  fash_K: forall P Q, fash (P --> Q) |-- fash P --> fash Q;
  fash_derives: forall P Q, P |-- Q -> fash P |-- fash Q;
  unfash_derives:  forall P Q,  P |-- Q -> unfash P |-- unfash Q;
  later_fash:  forall P, later (fash P) = fash (later P);
  later_unfash:  forall P, later (unfash P) = unfash (later P);
  fash_andp: forall P Q, fash (P && Q) = fash P && fash Q;
  unfash_allp:  forall {B} (P: B -> Triv), unfash (allp P) = ALL x:B, unfash (P x);  subp_allp: forall G B (X Y:B -> A),  (forall x:B, G |-- fash (imp (X x) (Y x))) ->  G |-- fash (imp (allp X) (allp Y));
  subp_exp: forall G B (X Y:B -> A),  (forall x:B, G |-- fash (imp (X x) (Y x))) ->  G |-- fash (imp (exp X) (exp Y));
  subp_e: forall (P Q : A), TT |-- fash (P --> Q) -> P |-- Q;
  subp_i1: forall P (Q R: A), unfash P && Q |-- R -> P |-- fash (Q --> R);
 fash_TT: forall G, G |-- fash TT;
  HOcontractive: forall {X: Type} (f: (X -> A) -> (X -> A)), Prop :=
         fun {X} f => forall P Q,  (ALL x:X, later (fash (P x <--> Q x))) |-- (ALL x:X, fash (f P x <--> f Q x));
  HORec_fold_unfold : forall X (f: (X -> A) -> (X -> A)) (H: HOcontractive f), HORec f = f (HORec f)
}.

Definition HOnonexpansive {A}{NA: NatDed A}{IA: Indir A}{RA: RecIndir A}
        {X: Type} (f: (X -> A) -> (X -> A)) :=
         forall P Q: X -> A,  (ALL x:X, fash (P x <--> Q x)) |-- (ALL x:X, fash (f P x <--> f Q x)).
End SL2.


Notation "'#' e" := (fash e) (at level 30, right associativity): logic.
Notation "'!' e" := (unfash e) (at level 30, right associativity): logic.
Notation "P '>=>' Q" := (# (P --> Q)) (at level 55, right associativity) : logic.
Notation "P '<=>' Q" := (# (P <--> Q)) (at level 57, no associativity) : logic.

Definition algRecIndir (T: Type) {agT: ageable T}{JoinT: Join T}{PermT: Perm_alg T}{SepT: Sep_alg T}{AgeT: Age_alg T} :
         @RecIndir (pred T) (algNatDed T) (algIndir T).
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@exp T agT T0 F)) (@orp T agT (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@imp T agT P Q)) (@imp T agT (@box T agT (@laterM T agT) P) (@box T agT (@laterM T agT) Q)) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@prop T agT PP)) (@orp T agT (@prop T agT PP) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @derives T agT (@prop T agT True) P *)
 apply (mkRecIndir _ _ _ subtypes.fash subtypes.unfash HoRec.HORec); intros; simpl.
(* Goal: @derives T agT (@subtypes.unfash T agT (@subtypes.fash T agT P)) P *)
(* Goal: @derives nat ag_nat (@subtypes.fash T agT (@imp T agT P Q)) (@imp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @derives nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q) *)
(* Goal: @derives T agT (@subtypes.unfash T agT P) (@subtypes.unfash T agT Q) *)
(* Goal: @eq Triv (@box nat ag_nat (@laterM nat ag_nat) (@subtypes.fash T agT P)) (@subtypes.fash T agT (@box T agT (@laterM T agT) P)) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@subtypes.unfash T agT P)) (@subtypes.unfash T agT (@box nat ag_nat (@laterM nat ag_nat) P)) *)
(* Goal: @eq Triv (@subtypes.fash T agT (@andp T agT P Q)) (@andp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @eq (@pred T agT) (@subtypes.unfash T agT (@allp nat ag_nat B P)) (@allp T agT B (fun x : B => @subtypes.unfash T agT (P x))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@allp T agT B X) (@allp T agT B Y))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@exp T agT B X) (@exp T agT B Y))) *)
(* Goal: @derives T agT P Q *)
(* Goal: @derives nat ag_nat P (@subtypes.fash T agT (@imp T agT Q R)) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@prop T agT True)) *)
(* Goal: @eq (forall _ : X, @pred T agT) (@HoRec.HORec T agT X f) (f (@HoRec.HORec T agT X f)) *)
 repeat intro. do 3 red in H. apply H; auto.
(* Goal: @derives nat ag_nat (@subtypes.fash T agT (@imp T agT P Q)) (@imp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @derives nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q) *)
(* Goal: @derives T agT (@subtypes.unfash T agT P) (@subtypes.unfash T agT Q) *)
(* Goal: @eq Triv (@box nat ag_nat (@laterM nat ag_nat) (@subtypes.fash T agT P)) (@subtypes.fash T agT (@box T agT (@laterM T agT) P)) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@subtypes.unfash T agT P)) (@subtypes.unfash T agT (@box nat ag_nat (@laterM nat ag_nat) P)) *)
(* Goal: @eq Triv (@subtypes.fash T agT (@andp T agT P Q)) (@andp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @eq (@pred T agT) (@subtypes.unfash T agT (@allp nat ag_nat B P)) (@allp T agT B (fun x : B => @subtypes.unfash T agT (P x))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@allp T agT B X) (@allp T agT B Y))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@exp T agT B X) (@exp T agT B Y))) *)
(* Goal: @derives T agT P Q *)
(* Goal: @derives nat ag_nat P (@subtypes.fash T agT (@imp T agT Q R)) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@prop T agT True)) *)
(* Goal: @eq (forall _ : X, @pred T agT) (@HoRec.HORec T agT X f) (f (@HoRec.HORec T agT X f)) *)
 apply @subtypes.fash_K.
(* Goal: le y a *)
 apply @subtypes.fash_derives; auto.
(* Goal: @derives T agT (@subtypes.unfash T agT P) (@subtypes.unfash T agT Q) *)
(* Goal: @eq Triv (@box nat ag_nat (@laterM nat ag_nat) (@subtypes.fash T agT P)) (@subtypes.fash T agT (@box T agT (@laterM T agT) P)) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@subtypes.unfash T agT P)) (@subtypes.unfash T agT (@box nat ag_nat (@laterM nat ag_nat) P)) *)
(* Goal: @eq Triv (@subtypes.fash T agT (@andp T agT P Q)) (@andp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @eq (@pred T agT) (@subtypes.unfash T agT (@allp nat ag_nat B P)) (@allp T agT B (fun x : B => @subtypes.unfash T agT (P x))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@allp T agT B X) (@allp T agT B Y))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@exp T agT B X) (@exp T agT B Y))) *)
(* Goal: @derives T agT P Q *)
(* Goal: @derives nat ag_nat P (@subtypes.fash T agT (@imp T agT Q R)) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@prop T agT True)) *)
(* Goal: @eq (forall _ : X, @pred T agT) (@HoRec.HORec T agT X f) (f (@HoRec.HORec T agT X f)) *)
 intros ? ?. do 3 red in H0. apply H in H0. apply H0.
(* Goal: le y a *)
 apply @subtypes.later_fash; auto.
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@subtypes.unfash T agT P)) (@subtypes.unfash T agT (@box nat ag_nat (@laterM nat ag_nat) P)) *)
(* Goal: @eq Triv (@subtypes.fash T agT (@andp T agT P Q)) (@andp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @eq (@pred T agT) (@subtypes.unfash T agT (@allp nat ag_nat B P)) (@allp T agT B (fun x : B => @subtypes.unfash T agT (P x))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@allp T agT B X) (@allp T agT B Y))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@exp T agT B X) (@exp T agT B Y))) *)
(* Goal: @derives T agT P Q *)
(* Goal: @derives nat ag_nat P (@subtypes.fash T agT (@imp T agT Q R)) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@prop T agT True)) *)
(* Goal: @eq (forall _ : X, @pred T agT) (@HoRec.HORec T agT X f) (f (@HoRec.HORec T agT X f)) *)
 apply @subtypes.later_unfash.
(* Goal: @eq Triv (@subtypes.fash T agT (@andp T agT P Q)) (@andp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @eq (@pred T agT) (@subtypes.unfash T agT (@allp nat ag_nat B P)) (@allp T agT B (fun x : B => @subtypes.unfash T agT (P x))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@allp T agT B X) (@allp T agT B Y))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@exp T agT B X) (@exp T agT B Y))) *)
(* Goal: @derives T agT P Q *)
(* Goal: @derives nat ag_nat P (@subtypes.fash T agT (@imp T agT Q R)) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@prop T agT True)) *)
(* Goal: @eq (forall _ : X, @pred T agT) (@HoRec.HORec T agT X f) (f (@HoRec.HORec T agT X f)) *)
 apply @subtypes.fash_and.
(* Goal: le y a *)
 apply pred_ext; repeat intro; do 3 red in H; apply (H b); auto.
(* Goal: le y a *)
 apply @subtypes.subp_allp; auto.
(* Goal: le y a *)
 eapply @subtypes.subp_exp; auto.
(* Goal: le y a *)
 eapply @subtypes.subp_e; eauto.
(* Goal: le y a *)
 eapply @subtypes.subp_i1; eauto.
(* Goal: @app_pred T agT (@prop T agT P) a *)
(* Goal: forall P Q : Prop, @derives T agT (@imp T agT (@prop T agT P) (@prop T agT Q)) (@prop T agT (forall _ : P, Q)) *)
(* Goal: forall (B : Type) (P : forall _ : B, Prop), @derives T agT (@allp T agT B (fun b : B => @prop T agT (P b))) (@prop T agT (forall b : B, P b)) *)
 repeat intro; hnf; auto.
(* Goal: le y a *)
 intros. apply HoRec.HORec_fold_unfold; auto.
Defined.

Instance TrivRecIndir: RecIndir Triv := algRecIndir nat.

Section SL3. Import VST.msl.seplog.

Lemma fash_triv: forall P: Triv, fash P = P.
Proof.
(* Goal: forall P : Triv, @eq Triv (@fash Triv TrivNatDed TrivIndir TrivRecIndir P) P *)
 intros.
(* Goal: @derives T agT (@subtypes.unfash T agT P) (@subtypes.unfash T agT Q) *)
(* Goal: @eq Triv (@box nat ag_nat (@laterM nat ag_nat) (@subtypes.fash T agT P)) (@subtypes.fash T agT (@box T agT (@laterM T agT) P)) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@subtypes.unfash T agT P)) (@subtypes.unfash T agT (@box nat ag_nat (@laterM nat ag_nat) P)) *)
(* Goal: @eq Triv (@subtypes.fash T agT (@andp T agT P Q)) (@andp nat ag_nat (@subtypes.fash T agT P) (@subtypes.fash T agT Q)) *)
(* Goal: @eq (@pred T agT) (@subtypes.unfash T agT (@allp nat ag_nat B P)) (@allp T agT B (fun x : B => @subtypes.unfash T agT (P x))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@allp T agT B X) (@allp T agT B Y))) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@imp T agT (@exp T agT B X) (@exp T agT B Y))) *)
(* Goal: @derives T agT P Q *)
(* Goal: @derives nat ag_nat P (@subtypes.fash T agT (@imp T agT Q R)) *)
(* Goal: @derives nat ag_nat G (@subtypes.fash T agT (@prop T agT True)) *)
(* Goal: @eq (forall _ : X, @pred T agT) (@HoRec.HORec T agT X f) (f (@HoRec.HORec T agT X f)) *)
 apply pred_ext; intros ? ?.
(* Goal: le y a *)
 eapply H. unfold level; simpl.  unfold natLevel; auto.
(* Goal: forall P : Triv, @eq Triv (@fash Triv TrivNatDed TrivIndir TrivRecIndir P) P *)
 hnf; intros. eapply pred_nec_hereditary; try eapply H.
(* Goal: le y a *)
 apply nec_nat. auto.
Qed.

Class SepRec  (A: Type) {NA: NatDed A}{SA: SepLog A}{IA: Indir A}{RA: RecIndir A} := mkSepRec {
  unfash_sepcon_distrib: forall (P: Triv) (Q R: A),
                 andp (unfash P) (sepcon Q R) = sepcon (andp (unfash P) Q) (andp (unfash P) R)
}.

End SL3.

Instance algSepIndir (T: Type) {agT: ageable T}{JoinT: Join T}{PermT: Perm_alg T}{SepT: Sep_alg T}{AgeT: Age_alg T} :
         @SepIndir (pred T) (algNatDed T) (algSepLog T) (algIndir T).
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@exp T agT T0 F)) (@orp T agT (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@imp T agT P Q)) (@imp T agT (@box T agT (@laterM T agT) P) (@box T agT (@laterM T agT) Q)) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@prop T agT PP)) (@orp T agT (@prop T agT PP) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @derives T agT (@prop T agT True) P *)
 apply mkSepIndir; simpl.
(* Goal: le y a *)
 apply @predicates_sl.later_sepcon; auto.
(* Goal: le y a *)
 apply @predicates_sl.later_wand; auto.
(* Goal: le y a *)
 apply @predicates_sl.later_ewand; auto.
Qed.

Instance algSepRec (T: Type) {agT: ageable T}{JoinT: Join T}{PermT: Perm_alg T}{SepT: Sep_alg T}{AgeT: Age_alg T} :
         @SepRec (pred T) (algNatDed T) (algSepLog T) (algIndir T)(algRecIndir T).
(* Goal: @SepRec (@pred T agT) (@algNatDed T agT) (@algSepLog T agT JoinT PermT SepT AgeT) (@algIndir T agT JoinT PermT SepT AgeT) (@algRecIndir T agT JoinT PermT SepT AgeT) *)
constructor.
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@exp T agT T0 F)) (@orp T agT (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@imp T agT P Q)) (@imp T agT (@box T agT (@laterM T agT) P) (@box T agT (@laterM T agT) Q)) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@prop T agT PP)) (@orp T agT (@prop T agT PP) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @derives T agT (@prop T agT True) P *)
 intros; simpl. apply subtypes_sl.unfash_sepcon_distrib.
Qed.

Instance algCorableSepLog (T: Type) {agT: ageable T}{JoinT: Join T}{PermT: Perm_alg T}{SepT: Sep_alg T}{AgeT: Age_alg T} :
         @CorableSepLog (pred T) (algNatDed T) (algSepLog T).
(* Goal: @CorableSepLog (@pred T agT) (@algNatDed T agT) (@algSepLog T agT JoinT PermT SepT AgeT) *)
  apply mkCorableSepLog with (corable := corable.corable).
  + apply corable.corable_prop.
  + apply corable.corable_andp.
  + apply corable.corable_orp.
  + apply corable.corable_imp.
(* Goal: le y a *)
  + intros; apply corable.corable_allp; auto.
(* Goal: le y a *)
  + intros; apply corable.corable_exp; auto.
  + apply corable.corable_sepcon.
  + apply corable.corable_wand.
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@exp T agT T0 F)) (@orp T agT (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@imp T agT P Q)) (@imp T agT (@box T agT (@laterM T agT) P) (@box T agT (@laterM T agT) Q)) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@prop T agT PP)) (@orp T agT (@prop T agT PP) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @derives T agT (@prop T agT True) P *)
  + intros; simpl.
(* Goal: le y a *)
    apply corable.corable_andp_sepcon1; auto.
Defined.

Instance algCorableIndir (T: Type) {agT: ageable T}{JoinT: Join T}{PermT: Perm_alg T}{SepT: Sep_alg T}{AgeT: Age_alg T} :
         @CorableIndir (pred T) (algNatDed T) (algSepLog T) (algCorableSepLog T) (algIndir T).
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@exp T agT T0 F)) (@orp T agT (@exp T agT T0 (fun x : T0 => @box T agT (@laterM T agT) (F x))) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @eq (@pred T agT) (@box T agT (@laterM T agT) (@imp T agT P Q)) (@imp T agT (@box T agT (@laterM T agT) P) (@box T agT (@laterM T agT) Q)) *)
(* Goal: @derives T agT (@box T agT (@laterM T agT) (@prop T agT PP)) (@orp T agT (@prop T agT PP) (@box T agT (@laterM T agT) (@prop T agT False))) *)
(* Goal: @derives T agT (@prop T agT True) P *)
  unfold CorableIndir; simpl.
(* Goal: forall (P : @pred T agT) (_ : @corable.corable T JoinT PermT SepT agT AgeT P), @corable.corable T JoinT PermT SepT agT AgeT (@box T agT (@laterM T agT) P) *)
  apply corable.corable_later.
Defined.