(*
 * Copyright (c) 2009-2010, Andrew Appel, Robert Dockins and Aquinas Hobor.
 *
 *)

Require Import VST.msl.base.
Require Import VST.msl.ageable.
Require Import VST.msl.sepalg.
Require Import VST.msl.sepalg_generators.
Require Import VST.msl.age_sepalg.
Require Import VST.msl.predicates_hered.
Require Import VST.msl.predicates_rec.
Require Import VST.msl.predicates_sl.
Require Import VST.msl.subtypes.
Require Import VST.msl.subtypes_sl.

Local Open Scope pred.

Lemma conj_nonexpansive {A} `{ageable A} : forall (F G:pred A -> pred A),
  nonexpansive F ->
  nonexpansive G ->
  nonexpansive (fun x:pred A => F x && G x).
Proof.
(* Goal: forall (F G : forall _ : @pred A AG, @pred A AG) (_ : @nonexpansive A AG F) (_ : @nonexpansive A AG G), @nonexpansive A AG (fun x : @pred A AG => @wand A JA PA AG XA (F x) (G x)) *)
  unfold nonexpansive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@andp A H (F P) (G P)) (@andp A H (F Q) (G Q)))) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@andp A H (F Q) (G Q)) (@andp A H (F P) (G P)))) *)
  apply subp_andp; apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@andp A H (F Q) (G Q)) (@andp A H (F P) (G P)))) *)
  apply subp_andp; apply eqp_subp2; auto.
Qed.

Lemma conj_contractive {A} `{ageable A} : forall F G,
  contractive F ->
  contractive G ->
  contractive (fun x => F x && G x).
Proof.
(* Goal: @contractive A H (@box A H (@laterM A H)) *)
  unfold contractive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@andp A H (F P) (G P)) (@andp A H (F Q) (G Q)))) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@andp A H (F Q) (G Q)) (@andp A H (F P) (G P)))) *)
  apply subp_andp; apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@andp A H (F Q) (G Q)) (@andp A H (F P) (G P)))) *)
  apply subp_andp; apply eqp_subp2; auto.
Qed.

Lemma impl_contractive {A} `{ageable A} : forall F G,
  contractive F ->
  contractive G ->
  contractive (fun x => F x --> G x).
Proof.
(* Goal: @contractive A H (@box A H (@laterM A H)) *)
  unfold contractive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H (@imp A H (F Q) (G Q)) (@imp A H (F P) (G P)))) *)
  apply subp_imp.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H (@imp A H (F Q) (G Q)) (@imp A H (F P) (G P)))) *)
  apply subp_imp.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
Qed.

Lemma impl_nonexpansive {A} `{ageable A} : forall F G,
  nonexpansive F ->
  nonexpansive G ->
  nonexpansive (fun x => F x --> G x).
Proof.
(* Goal: forall (F G : forall _ : @pred A AG, @pred A AG) (_ : @nonexpansive A AG F) (_ : @nonexpansive A AG G), @nonexpansive A AG (fun x : @pred A AG => @wand A JA PA AG XA (F x) (G x)) *)
  unfold nonexpansive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H (@imp A H (F Q) (G Q)) (@imp A H (F P) (G P)))) *)
  apply subp_imp.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H (@imp A H (F Q) (G Q)) (@imp A H (F P) (G P)))) *)
  apply subp_imp.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
Qed.

Lemma forall_contractive {A} `{ageable A} : forall B (X : pred A -> B -> pred A),
  (forall x, (contractive (fun y => X y x))) ->
  contractive (fun x => (allp (X x))).
Proof.
(* Goal: @contractive A H (@box A H (@laterM A H)) *)
  unfold contractive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H (@allp A H B (X Q)) (@allp A H B (X P)))) *)
  apply subp_allp; intros.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H (@allp A H B (X Q)) (@allp A H B (X P)))) *)
  apply subp_allp; intros.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
Qed.

Lemma forall_nonexpansive {A} `{ageable A} : forall B (X : pred A -> B -> pred A),
  (forall x, (nonexpansive (fun y => X y x))) ->
  nonexpansive (fun x => (allp (X x))).
Proof.
(* Goal: forall (F G : forall _ : @pred A AG, @pred A AG) (_ : @nonexpansive A AG F) (_ : @nonexpansive A AG G), @nonexpansive A AG (fun x : @pred A AG => @wand A JA PA AG XA (F x) (G x)) *)
  unfold nonexpansive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H (@allp A H B (X Q)) (@allp A H B (X P)))) *)
  apply subp_allp; intros.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H (@allp A H B (X Q)) (@allp A H B (X P)))) *)
  apply subp_allp; intros.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
Qed.

Lemma exists_contractive {A} `{ageable A} : forall B (X : pred A -> B -> pred A),
  (forall x, (contractive (fun y => X y x))) ->
  contractive (fun x => (exp (X x))).
Proof.
(* Goal: @contractive A H (@box A H (@laterM A H)) *)
  unfold contractive; intros.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@andp A H (@imp A H (@exp A H B (X P)) (@exp A H B (X Q))) (@imp A H (@exp A H B (X Q)) (@exp A H B (X P))))) *)
  apply subp_eqp; apply subp_exp; intros.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
Qed.

Lemma exists_nonexpansive {A} `{ageable A} : forall B (X : pred A -> B -> pred A),
  (forall x, (nonexpansive (fun y => X y x))) ->
  nonexpansive (fun x => (exp (X x))).
Proof.
(* Goal: forall (F G : forall _ : @pred A AG, @pred A AG) (_ : @nonexpansive A AG F) (_ : @nonexpansive A AG G), @nonexpansive A AG (fun x : @pred A AG => @wand A JA PA AG XA (F x) (G x)) *)
  unfold nonexpansive; intros.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@andp A H (@imp A H (@exp A H B (X P)) (@exp A H B (X Q))) (@imp A H (@exp A H B (X Q)) (@exp A H B (X P))))) *)
  apply subp_eqp; apply subp_exp; intros.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
Qed.

Lemma later_contractive {A} `{ageable A} : forall F,
  nonexpansive F ->
  contractive (fun X => (|>(F X))).
Proof.
(* Goal: forall (F : forall _ : @pred A H, @pred A H) (_ : @nonexpansive A H F), @contractive A H (fun X : @pred A H => @box A H (@laterM A H) (F X)) *)
  unfold nonexpansive, contractive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  rewrite <- subp_later.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@imp A H Q P))) *)
  apply box_positive; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  rewrite <- subp_later.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@imp A H Q P))) *)
  apply box_positive; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
Qed.

Lemma const_nonexpansive {A: Type} {H: ageable A}: forall P: pred A,
  nonexpansive (fun _ => P).
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  intros.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  hnf; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P0 Q) (@imp A H Q P0)))) (@fash A H (@andp A H (@imp A H P P) (@imp A H P P))) *)
  intros w ? ? ?.
(* Goal: @app_pred A H (@andp A H (@imp A H P P) (@imp A H P P)) y *)
  clear.
(* Goal: @app_pred A H (@andp A H (@imp A H P P) (@imp A H P P)) y *)
  hnf; split; intros ? ? ?; auto.
Qed.

Lemma const_contractive {A: Type} {H: ageable A}: forall P: pred A,
  contractive (fun _ => P).
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  intros.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  hnf; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P0 Q) (@imp A H Q P0)))) (@fash A H (@andp A H (@imp A H P P) (@imp A H P P))) *)
  intros w ? ? ?.
(* Goal: @app_pred A H (@andp A H (@imp A H P P) (@imp A H P P)) y *)
  clear.
(* Goal: @app_pred A H (@andp A H (@imp A H P P) (@imp A H P P)) y *)
  hnf; split; intros ? ? ?; auto.
Qed.

Lemma identity_nonexpansive {A: Type} {H: ageable A}:
  nonexpansive (fun P: pred A => P).
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  hnf; intros.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) *)
  intros ?; auto.
Qed.

(*
Lemma box_contractive {A} `{ageable A} : forall F (M:modality),
  inclusion _ M fashionR ->
  contractive F ->
  contractive (fun X => box M (F X)).
Proof.
(* Goal: @contractive A H (@box A H (@laterM A H)) *)
  unfold contractive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  apply sub_box; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  apply sub_box; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
Qed.

Lemma box_nonexpansive {A} `{ageable A} : forall F (M:modality),
  inclusion _ M fashionR ->
  nonexpansive F ->
  nonexpansive (fun X => box M (F X)).
Proof.
(* Goal: forall (F G : forall _ : @pred A AG, @pred A AG) (_ : @nonexpansive A AG F) (_ : @nonexpansive A AG G), @nonexpansive A AG (fun x : @pred A AG => @wand A JA PA AG XA (F x) (G x)) *)
  unfold nonexpansive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  apply sub_box; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  apply sub_box; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
Qed.

Lemma diamond_contractive {A} `{ageable A} : forall F (M:modality),
  inclusion _ M fashionR ->
  contractive F ->
  contractive (fun X => diamond M (F X)).
Proof.
(* Goal: @contractive A H (@box A H (@laterM A H)) *)
  unfold contractive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  apply sub_diamond; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  apply sub_diamond; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
Qed.

Lemma diamond_nonexpansive {A} `{ageable A} : forall F (M:modality),
  inclusion _ M fashionR ->
  nonexpansive F ->
  nonexpansive (fun X => diamond M (F X)).
Proof.
(* Goal: forall (F G : forall _ : @pred A AG, @pred A AG) (_ : @nonexpansive A AG F) (_ : @nonexpansive A AG G), @nonexpansive A AG (fun x : @pred A AG => @wand A JA PA AG XA (F x) (G x)) *)
  unfold nonexpansive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  apply sub_diamond; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  apply sub_diamond; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
Qed.
*)

Lemma contractive_nonexpansive {A} `{ageable A} : forall F,
  contractive F ->
  nonexpansive F.
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  unfold contractive, nonexpansive; intros.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@andp A H (@imp A H (F P) (F Q)) (@imp A H (F Q) (F P)))) *)
  apply @derives_trans with (|>(P <=>Q)); auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) *)
  apply now_later.
Qed.

Lemma sepcon_contractive {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : forall F G,
  contractive F ->
  contractive G ->
  contractive (fun x => F x * G x).
Proof.
(* Goal: @contractive A H (@box A H (@laterM A H)) *)
  unfold contractive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply subp_sepcon; apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply subp_sepcon; apply eqp_subp2; auto.
Qed.

Lemma sepcon_nonexpansive {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : forall F G,
  nonexpansive F ->
  nonexpansive G ->
  nonexpansive (fun x => F x * G x).
Proof.
(* Goal: forall (F G : forall _ : @pred A AG, @pred A AG) (_ : @nonexpansive A AG F) (_ : @nonexpansive A AG G), @nonexpansive A AG (fun x : @pred A AG => @wand A JA PA AG XA (F x) (G x)) *)
  unfold nonexpansive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply subp_sepcon; apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply subp_sepcon; apply eqp_subp2; auto.
Qed.

Lemma wand_contractive {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : forall F G,
  contractive F ->
  contractive G ->
  contractive (fun x => F x -* G x).
Proof.
(* Goal: @contractive A H (@box A H (@laterM A H)) *)
  unfold contractive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@fash A AG (@andp A AG (@imp A AG P Q) (@imp A AG Q P))) (@fash A AG (@imp A AG (@wand A JA PA AG XA (F Q) (G Q)) (@wand A JA PA AG XA (F P) (G P)))) *)
  apply sub_wand.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A AG (@andp A AG (@imp A AG P Q) (@imp A AG Q P))) (@fash A AG (@imp A AG (@wand A JA PA AG XA (F Q) (G Q)) (@wand A JA PA AG XA (F P) (G P)))) *)
  apply sub_wand.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
Qed.

Lemma wand_nonexpansive {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : forall F G,
  nonexpansive F ->
  nonexpansive G ->
  nonexpansive (fun x => F x -* G x).
Proof.
(* Goal: forall (F G : forall _ : @pred A AG, @pred A AG) (_ : @nonexpansive A AG F) (_ : @nonexpansive A AG G), @nonexpansive A AG (fun x : @pred A AG => @wand A JA PA AG XA (F x) (G x)) *)
  unfold nonexpansive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@fash A AG (@andp A AG (@imp A AG P Q) (@imp A AG Q P))) (@fash A AG (@imp A AG (@wand A JA PA AG XA (F Q) (G Q)) (@wand A JA PA AG XA (F P) (G P)))) *)
  apply sub_wand.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A AG (@andp A AG (@imp A AG P Q) (@imp A AG Q P))) (@fash A AG (@imp A AG (@wand A JA PA AG XA (F Q) (G Q)) (@wand A JA PA AG XA (F P) (G P)))) *)
  apply sub_wand.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
Qed.

Lemma prove_contractive {A} `{ageable A} : forall F,
  (forall P Q,
    |>(P >=> Q) |-- F P >=> F Q) ->
  contractive F.
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  intros.
(* Goal: @contractive A H F *)
  unfold contractive.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (F P) (F Q))) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (F Q) (F P))) *)
  apply @derives_trans with (|>(P >=> Q)).
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@imp A H Q P))) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@imp A H Q P))) (@fash A H (@imp A H (F Q) (F P))) *)
  apply box_positive.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@imp A H P Q))) (@fash A H (@imp A H (F P) (F Q))) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (F Q) (F P))) *)
  apply eqp_subp.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@imp A H Q P))) (@fash A H (@imp A H (F Q) (F P))) *)
  hnf; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  auto.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (F Q) (F P))) *)
  apply @derives_trans with (|>(Q >=> P)).
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@imp A H Q P))) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@imp A H Q P))) (@fash A H (@imp A H (F Q) (F P))) *)
  apply box_positive.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@imp A H Q P))) (@fash A H (@imp A H (F Q) (F P))) *)
  apply eqp_subp2.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@imp A H Q P))) (@fash A H (@imp A H (F Q) (F P))) *)
  hnf; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  auto.
Qed.

Lemma prove_HOcontractive1 {A} `{ageable A} : forall X F,
  (forall P Q: X -> pred A,
    (ALL x:X, |>(P x >=> Q x) |--
        ALL x:X, F P x >=> F Q x)) ->
   HOcontractive F.
Proof.
(* Goal: forall (X : Type) (F : forall (_ : forall _ : X, @pred A H) (_ : X), @pred A H) (_ : forall (P Q : forall _ : X, @pred A H) (x : X), @derives nat ag_nat (@allp nat ag_nat X (fun x0 : X => @fash A H (@andp A H (@imp A H (@box A H (@laterM A H) (P x0)) (@box A H (@laterM A H) (Q x0))) (@imp A H (@box A H (@laterM A H) (Q x0)) (@box A H (@laterM A H) (P x0)))))) (@fash A H (@imp A H (F P x) (F Q x)))), @HOcontractive A H X F *)
  unfold HOcontractive.
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  repeat intro.
(* Goal: @app_pred A H (@andp A H (@imp A H (F P v) (F Q v)) (@imp A H (F Q v) (F P v))) y *)
  split.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H0; eauto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  repeat intro; eapply H1; eauto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H0; eauto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  repeat intro; eapply H1; eauto.
Qed.


Lemma prove_HOcontractive {A} `{ageable A} : forall X F,
  (forall (P Q: X -> pred A) (x: X),
    (ALL x:X, (|> P x <=> |> Q x) |-- F P x >=> F Q x)) ->
   HOcontractive F.
Proof.
(* Goal: forall (X : Type) (F : forall (_ : forall _ : X, @pred A H) (_ : X), @pred A H) (_ : forall (P Q : forall _ : X, @pred A H) (x : X), @derives nat ag_nat (@allp nat ag_nat X (fun x0 : X => @fash A H (@andp A H (@imp A H (@box A H (@laterM A H) (P x0)) (@box A H (@laterM A H) (Q x0))) (@imp A H (@box A H (@laterM A H) (Q x0)) (@box A H (@laterM A H) (P x0)))))) (@fash A H (@imp A H (F P x) (F Q x)))), @HOcontractive A H X F *)
  unfold HOcontractive.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  intros. apply allp_right. intros.
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  repeat intro.
(* Goal: @app_pred A H (@andp A H (@imp A H (F P v) (F Q v)) (@imp A H (F Q v) (F P v))) y *)
  split.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H0; eauto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  intro x; specialize (H1 x). apply eqp_later1. auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H0; eauto.
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A H (@andp A H (@imp A H (@box A H (@laterM A H) (Q x)) (@box A H (@laterM A H) (P x))) (@imp A H (@box A H (@laterM A H) (P x)) (@box A H (@laterM A H) (Q x)))))) a *)
  intro x; specialize (H1 x). rewrite eqp_comm.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  apply eqp_later1. auto.
Qed.

Ltac sub_unfold :=
   match goal with
    | |- _ |-- ?A _ >=> ?A _ => unfold A
    | |- _ |-- ?A _ _ >=> ?A _ _ => unfold A
    | |- _ |-- ?A _ _ _ >=> ?A _ _ _ => unfold A
    | |- _ |-- ?A _ _ _ _ >=> ?A _ _ _ _ => unfold A
    | |- _ |-- ?A _ _ _ _ _ >=> ?A _ _ _ _ _ => unfold A
    | v: _ |- _ => destruct v
   end.

Hint Extern 2 (_ |-- _ >=> _) => sub_unfold : contractive.

Hint Resolve @prove_HOcontractive
  @subp_allp @subp_imp @subp_refl @subp_exp @subp_andp @subp_orp @subp_subp
  @allp_imp2_later_e1 @allp_imp2_later_e2 : contractive.

Lemma Rec_sub {A} `{ageable A} : forall G
  (F   : pred A -> pred A -> pred A)
  (HF1 : forall X, contractive (F X))
  (HF2 : forall R P Q, P >=> Q |-- F P R >=> F Q R)
  (HF3 : forall P Q X, |>(P >=> Q) |-- F X P >=> F X Q),
  forall P Q,
    G |-- P >=> Q ->
    G |-- Rec (F P) >=> Rec (F Q).
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  intros.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  apply @derives_trans with (P >=> Q); auto.
(* Goal: @derives nat ag_nat (@fash A H (@imp A H P Q)) (@allp nat ag_nat B (fun b : B => @fash A H (@imp A H (@HORec A H B (F P) b) (@HORec A H B (F Q) b)))) *)
  clear H0.
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  apply goedel_loeb; repeat intro.
(* Goal: @app_pred A H (@andp A H (@imp A H (@HORec A H B (F P) b) (@HORec A H B (F Q) b)) (@imp A H (@HORec A H B (F Q) b) (@HORec A H B (F P) b))) y *)
  destruct H0.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite Rec_fold_unfold by auto.
(* Goal: @app_pred A H (F Q (@Rec A H (F Q))) a' *)
  specialize ( HF2 (Rec (F Q)) P Q).
(* Goal: @app_pred A H (F Q (@Rec A H (F Q))) a' *)
  specialize ( HF2 a H0 a').
(* Goal: ge a (@level A H a') *)
(* Goal: @app_pred A H (F P (@HORec A H B (F Q)) b) a' *)
  spec  HF2.  apply necR_level in H2; omega.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply HF2; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite Rec_fold_unfold in H3 by auto.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  generalize (HF3 (Rec (F P)) (Rec (F Q)) P); intros.
(* Goal: @app_pred A H (F P (@Rec A H (F Q))) a' *)
  specialize ( H5 a H4 a').
(* Goal: ge a (@level A H a') *)
(* Goal: @app_pred A H (F P (@HORec A H B (F Q)) b) a' *)
  spec H5.  apply necR_level in H2; omega.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H5; auto.
Qed.

Lemma HORec_sub {A} `{ageable A} : forall G B
  (F : pred A -> (B -> pred A) -> B -> pred A)
  (HF1 : forall X, HOcontractive (F X))
  (HF2 : forall R a P Q, P >=> Q |-- F P R a >=> F Q R a)
  (HF3 : forall P Q X, ALL b:B, |>(P b >=> Q b) |-- ALL b:B, F X P b >=> F X Q b),
  forall P Q,
    G |-- P >=> Q ->
    G |-- ALL b:B, HORec (F P) b >=> HORec (F Q) b.
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  intros.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  apply @derives_trans with (P>=>Q); auto.
(* Goal: @derives nat ag_nat (@fash A H (@imp A H P Q)) (@allp nat ag_nat B (fun b : B => @fash A H (@imp A H (@HORec A H B (F P) b) (@HORec A H B (F Q) b)))) *)
  clear H0.
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  apply goedel_loeb; repeat intro.
(* Goal: @app_pred A H (@andp A H (@imp A H (@HORec A H B (F P) b) (@HORec A H B (F Q) b)) (@imp A H (@HORec A H B (F Q) b) (@HORec A H B (F P) b))) y *)
  destruct H0.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite HORec_fold_unfold by auto.
(* Goal: @app_pred A H (F Q (@HORec A H B (F Q)) b) a' *)
(* Goal: @app_pred A H (@HORec A H B (F P) b) a' *)
  specialize ( HF2 (HORec (F Q)) b P Q a H0 a').
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  spec HF2. apply necR_level in H2; omega.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  apply HF2; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite HORec_fold_unfold in H3 by auto.
(* Goal: @app_pred A H (F P (@HORec A H B (F Q)) b) a' *)
  rewrite box_all in H4.
(* Goal: @app_pred A H (F P (@HORec A H B (F Q)) b) a' *)
  specialize ( HF3 (HORec (F P)) (HORec (F Q)) P a H4 b a').
(* Goal: ge a (@level A H a') *)
(* Goal: @app_pred A H (F P (@HORec A H B (F Q)) b) a' *)
  spec HF3. apply necR_level in H2; omega.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  apply HF3; auto.
Qed.

Lemma Rec_contractive {A} `{ageable A} : forall
  (F   : pred A -> pred A -> pred A)
  (HF1 : forall X, contractive (F X))
  (HF2 : forall R, contractive (fun X => F X R)),
  contractive (fun X => Rec (F X)).
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  intros; hnf; intros.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a)))) *)
  simpl.
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  apply goedel_loeb; repeat intro.
(* Goal: @app_pred A H (@andp A H (@imp A H (@HORec A H B (F P) b) (@HORec A H B (F Q) b)) (@imp A H (@HORec A H B (F Q) b) (@HORec A H B (F P) b))) y *)
  destruct H0.
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  split; repeat intro.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite Rec_fold_unfold by auto.
(* Goal: @app_pred A H (F Q (@Rec A H (F Q))) a' *)
(* Goal: @app_pred A H (@Rec A H (F P)) a' *)
  specialize ( HF2 (Rec (F Q)) P Q a H0 a').
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  spec HF2. apply necR_level in H3; omega.
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  destruct HF2.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H5; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite Rec_fold_unfold in H4 by auto.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  generalize (HF1 P (Rec (F P)) (Rec (F Q))); intros.
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
  specialize ( H7 a).
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  detach H7; auto.
(* Goal: ge a (@level A H a') *)
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat B (fun x : B => @box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) x) (@HORec A H B (F Q) x)) (@imp A H (@HORec A H B (F Q) x) (@HORec A H B (F P) x)))))) a *)
  specialize ( H7 a').  spec H7. apply necR_level in H3; omega.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  destruct H7; eauto.

(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite Rec_fold_unfold by auto.
(* Goal: @app_pred A H (F P (@Rec A H (F P))) a' *)
  specialize ( HF2 (Rec (F P)) P Q a H0 a').
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  spec HF2. apply necR_level in H3; omega.
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  destruct HF2.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H6; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite Rec_fold_unfold in H4 by auto.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  generalize (HF1 Q (Rec (F P)) (Rec (F Q))); intros.
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
  specialize ( H7 a).
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  detach H7; auto.
(* Goal: ge a (@level A H a') *)
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat B (fun x : B => @box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) x) (@HORec A H B (F Q) x)) (@imp A H (@HORec A H B (F Q) x) (@HORec A H B (F P) x)))))) a *)
  specialize ( H7 a').  spec H7. apply necR_level in H3; omega.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  destruct H7; eauto.
Qed.

Lemma Rec_nonexpansive {A} `{ageable A} : forall
  (F   : pred A -> pred A -> pred A)
  (HF1 : forall X, contractive (F X))
  (HF2 : forall R, nonexpansive (fun X => F X R)),
  nonexpansive (fun X => Rec (F X)).
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  intros; hnf; intros.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a)))) *)
  simpl.
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  apply goedel_loeb; repeat intro.
(* Goal: @app_pred A H (@andp A H (@imp A H (@HORec A H B (F P) b) (@HORec A H B (F Q) b)) (@imp A H (@HORec A H B (F Q) b) (@HORec A H B (F P) b))) y *)
  destruct H0.
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  split; repeat intro.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite Rec_fold_unfold by auto.
(* Goal: @app_pred A H (F Q (@Rec A H (F Q))) a' *)
(* Goal: @app_pred A H (@Rec A H (F P)) a' *)
  specialize ( HF2 (Rec (F Q)) P Q a H0 a').
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  spec HF2. apply necR_level in H3; omega.
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  destruct HF2.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H5; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite Rec_fold_unfold in H4 by auto.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  generalize (HF1 P (Rec (F P)) (Rec (F Q))); intros.
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
  specialize ( H7 a).
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  detach H7; auto.
(* Goal: ge a (@level A H a') *)
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat B (fun x : B => @box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) x) (@HORec A H B (F Q) x)) (@imp A H (@HORec A H B (F Q) x) (@HORec A H B (F P) x)))))) a *)
  specialize ( H7 a').  spec H7. apply necR_level in H3; omega.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  destruct H7; eauto.

(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite Rec_fold_unfold by auto.
(* Goal: @app_pred A H (F P (@Rec A H (F P))) a' *)
  specialize ( HF2 (Rec (F P)) P Q a H0 a').
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  spec HF2. apply necR_level in H3; omega.
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  destruct HF2.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H6; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite Rec_fold_unfold in H4 by auto.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  generalize (HF1 Q (Rec (F P)) (Rec (F Q))); intros.
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
  specialize ( H7 a).
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  detach H7; auto.
(* Goal: ge a (@level A H a') *)
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat B (fun x : B => @box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) x) (@HORec A H B (F Q) x)) (@imp A H (@HORec A H B (F Q) x) (@HORec A H B (F P) x)))))) a *)
  specialize ( H7 a').  spec H7. apply necR_level in H3; omega.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  destruct H7; eauto.
Qed.


Lemma HORec_contractive {A} `{ageable A} : forall B
  (F : pred A -> (B -> pred A) -> B -> pred A)
  (HF1 : forall X, HOcontractive (F X))
  (HF2 : forall R a, contractive (fun X => F X R a)),
  forall a, contractive (fun X => HORec (F X) a).
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  intros; hnf; intros.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a)))) *)
  simpl.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a)))) *)
  cut (|>(P <=> Q) |-- ALL a:B, HORec (F P) a <=> HORec (F Q) a).
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  repeat intro.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H0; eauto.

(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  clear a.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  apply goedel_loeb.
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  repeat intro.
(* Goal: @app_pred A H (@andp A H (@imp A H (@HORec A H B (F P) b) (@HORec A H B (F Q) b)) (@imp A H (@HORec A H B (F Q) b) (@HORec A H B (F P) b))) y *)
  destruct H0.
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  split; repeat intro.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite HORec_fold_unfold by auto.
(* Goal: @app_pred A H (F Q (@HORec A H B (F Q)) b) a' *)
(* Goal: @app_pred A H (@HORec A H B (F P) b) a' *)
  specialize ( HF2 (HORec (F Q)) b P Q a H0 a').
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  spec HF2. apply necR_level in H3; omega.
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  destruct HF2.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H5; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite HORec_fold_unfold in H4 by auto.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  generalize (HF1 P (HORec (F P)) (HORec (F Q))); intros.
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
  specialize ( H7 a).
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
  detach H7.
(* Goal: ge a (@level A H a') *)
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat B (fun x : B => @box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) x) (@HORec A H B (F Q) x)) (@imp A H (@HORec A H B (F Q) x) (@HORec A H B (F P) x)))))) a *)
  specialize ( H7 b a').  spec H7. apply necR_level in H3; omega.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  destruct H7; eauto.
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat B (fun x : B => @box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) x) (@HORec A H B (F Q) x)) (@imp A H (@HORec A H B (F Q) x) (@HORec A H B (F P) x)))))) a *)
  rewrite <- box_all.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  auto.

(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite HORec_fold_unfold by auto.
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  specialize ( HF2 (HORec (F P)) b P Q a H0 a').
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  spec HF2. apply necR_level in H3; omega.
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  destruct HF2.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H6; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite HORec_fold_unfold in H4 by auto.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  generalize (HF1 Q (HORec (F P)) (HORec (F Q))); intros.
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
  specialize ( H7 a).
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
  detach H7.
(* Goal: ge a (@level A H a') *)
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat B (fun x : B => @box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) x) (@HORec A H B (F Q) x)) (@imp A H (@HORec A H B (F Q) x) (@HORec A H B (F P) x)))))) a *)
  specialize ( H7 b a').  spec H7. apply necR_level in H3; omega.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  destruct H7; eauto.
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat B (fun x : B => @box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) x) (@HORec A H B (F Q) x)) (@imp A H (@HORec A H B (F Q) x) (@HORec A H B (F P) x)))))) a *)
  rewrite <- box_all.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  auto.
Qed.

Lemma HORec_nonexpansive {A} `{ageable A} : forall B
  (F : pred A -> (B -> pred A) -> B -> pred A)
  (HF1 : forall X, HOcontractive (F X))
  (HF2 : forall R a, nonexpansive (fun X => F X R a)),
  forall a, nonexpansive (fun X => HORec (F X) a).
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  intros; hnf; intros.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a)))) *)
  simpl.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a)))) *)
  cut (P <=> Q |-- ALL a:B, HORec (F P) a <=> HORec (F Q) a).
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  repeat intro.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H0; eauto.

(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  clear a.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  apply goedel_loeb.
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  repeat intro.
(* Goal: @app_pred A H (@andp A H (@imp A H (@HORec A H B (F P) b) (@HORec A H B (F Q) b)) (@imp A H (@HORec A H B (F Q) b) (@HORec A H B (F P) b))) y *)
  destruct H0.
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@box nat ag_nat (@laterM nat ag_nat) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))))) (@allp nat ag_nat B (fun a : B => @fash A H (@andp A H (@imp A H (@HORec A H B (F P) a) (@HORec A H B (F Q) a)) (@imp A H (@HORec A H B (F Q) a) (@HORec A H B (F P) a))))) *)
  split; repeat intro.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite HORec_fold_unfold by auto.
(* Goal: @app_pred A H (F Q (@HORec A H B (F Q)) b) a' *)
(* Goal: @app_pred A H (@HORec A H B (F P) b) a' *)
  specialize ( HF2 (HORec (F Q)) b P Q a H0 a').
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  spec HF2. apply necR_level in H3; omega.
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  destruct HF2.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H5; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite HORec_fold_unfold in H4 by auto.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  generalize (HF1 P (HORec (F P)) (HORec (F Q))); intros.
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
  specialize ( H7 a).
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
  detach H7.
(* Goal: ge a (@level A H a') *)
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat B (fun x : B => @box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) x) (@HORec A H B (F Q) x)) (@imp A H (@HORec A H B (F Q) x) (@HORec A H B (F P) x)))))) a *)
  specialize ( H7 b a').  spec H7. apply necR_level in H3; omega.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  destruct H7; eauto.
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat B (fun x : B => @box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) x) (@HORec A H B (F Q) x)) (@imp A H (@HORec A H B (F Q) x) (@HORec A H B (F P) x)))))) a *)
  rewrite <- box_all.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  auto.

(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite HORec_fold_unfold by auto.
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  specialize ( HF2 (HORec (F P)) b P Q a H0 a').
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  spec HF2. apply necR_level in H3; omega.
(* Goal: @app_pred A H (F P (@HORec A H B (F P)) b) a' *)
  destruct HF2.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  eapply H6; auto.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  rewrite HORec_fold_unfold in H4 by auto.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
  generalize (HF1 Q (HORec (F P)) (HORec (F Q))); intros.
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
  specialize ( H7 a).
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
  detach H7.
(* Goal: ge a (@level A H a') *)
(* Goal: @app_pred A H (F Q (@HORec A H B (F P)) b) a' *)
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat B (fun x : B => @box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) x) (@HORec A H B (F Q) x)) (@imp A H (@HORec A H B (F Q) x) (@HORec A H B (F P) x)))))) a *)
  specialize ( H7 b a').  spec H7. apply necR_level in H3; omega.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  destruct H7; eauto.
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat B (fun x : B => @box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H (@HORec A H B (F P) x) (@HORec A H B (F Q) x)) (@imp A H (@HORec A H B (F Q) x) (@HORec A H B (F P) x)))))) a *)
  rewrite <- box_all.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
  auto.
Qed.

Module Trashcan.

(* Note: This approach to proving HOcontractive doesn't automate
  as well as the methods above.*)

Lemma orp_HOcontractive {A}{agA: ageable A}: forall X (P Q: (X -> pred A) -> (X -> pred A)),
       HOcontractive P -> HOcontractive Q -> HOcontractive (fun R x => P R x || Q R x).
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
 intros.
(* Goal: @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @andp A agA (P R x) (Q R x)) *)
 intros F G n H2 x y Hy.
(* Goal: @app_pred A agA (@andp A agA (@imp A agA (@andp A agA (P F x) (Q F x)) (@andp A agA (P G x) (Q G x))) (@imp A agA (@andp A agA (P G x) (Q G x)) (@andp A agA (P F x) (Q F x)))) y *)
 specialize (H F G n H2 x y Hy). specialize (H0 F G n H2 x y Hy).
(* Goal: @app_pred A agA (@andp A agA (@imp A agA (@andp A agA (P F x) (Q F x)) (@andp A agA (P G x) (Q G x))) (@imp A agA (@andp A agA (P G x) (Q G x)) (@andp A agA (P F x) (Q F x)))) y *)
 destruct H, H0.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
 split; (intros z Hz [?|?]; [left|right]); auto.
Qed.
Lemma andp_HOcontractive {A}{agA: ageable A}: forall X (P Q: (X -> pred A) -> (X -> pred A)),
       HOcontractive P -> HOcontractive Q -> HOcontractive (fun R x => P R x && Q R x).
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
 intros.
(* Goal: @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @andp A agA (P R x) (Q R x)) *)
 intros F G n H2 x y Hy.
(* Goal: @app_pred A agA (@andp A agA (@imp A agA (@andp A agA (P F x) (Q F x)) (@andp A agA (P G x) (Q G x))) (@imp A agA (@andp A agA (P G x) (Q G x)) (@andp A agA (P F x) (Q F x)))) y *)
 specialize (H F G n H2 x y Hy). specialize (H0 F G n H2 x y Hy).
(* Goal: @app_pred A agA (@andp A agA (@imp A agA (@andp A agA (P F x) (Q F x)) (@andp A agA (P G x) (Q G x))) (@imp A agA (@andp A agA (P G x) (Q G x)) (@andp A agA (P F x) (Q F x)))) y *)
 destruct H, H0.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
 split; (intros z Hz [? ?]); split; auto.
Qed.
Lemma sepcon_HOcontractive {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}: forall X (P Q: (X -> pred A) -> (X -> pred A)),
       HOcontractive P -> HOcontractive Q -> HOcontractive (fun R x => P R x * Q R x).
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
 intros.
 unfold HOcontractive in *|-.
 apply prove_HOcontractive; intros F G ?.
 specialize (H F G). specialize (H0 F G).
 apply subp_sepcon.
 eapply derives_trans.
 apply allp_derives; intro. rewrite <- eqp_later. apply derives_refl.
 eapply derives_trans; [ apply H | ].
 apply allp_left with x.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
 apply fash_derives. apply andp_left1. auto.
 eapply derives_trans.
 apply allp_derives; intro. rewrite <- eqp_later. apply derives_refl.
 eapply derives_trans; [ apply H0 | ].
 apply allp_left with x.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
 apply fash_derives. apply andp_left1. auto.
Qed.

Lemma const_HOcontractive{A}{agA: ageable A}: forall X (P : X -> pred A), HOcontractive (fun _ => P).
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
 intros.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
 apply prove_HOcontractive. intros. apply subp_refl.
Qed.

Lemma exp_HOcontractive {A}{agA: ageable A}:
  forall X Y (G: Y -> X -> X) (F: Y -> X -> pred A -> pred A),
   (forall y x, contractive (F y x)) ->
   HOcontractive (fun (R: X -> pred A) (x: X) => EX y: Y, F y x (R (G y x))).
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
 intros.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
 apply prove_HOcontractive; intros.
(* Goal: @derives nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P x)) (@box A agA (@laterM A agA) (Q x))) (@imp A agA (@box A agA (@laterM A agA) (Q x)) (@box A agA (@laterM A agA) (P x)))))) (@fash A agA (@imp A agA (@exp A agA Y (fun y : Y => F y x (P (G y x)))) (@exp A agA Y (fun y : Y => F y x (Q (G y x)))))) *)
 apply subp_exp; intro y.
(* Goal: @derives nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P x)) (@box A agA (@laterM A agA) (Q x))) (@imp A agA (@box A agA (@laterM A agA) (Q x)) (@box A agA (@laterM A agA) (P x)))))) (@fash A agA (@imp A agA (F y x (P (G y x))) (F y x (Q (G y x))))) *)
 specialize (H y x (P (G y x)) (Q (G y x))).
(* Goal: @derives nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P x)) (@box A agA (@laterM A agA) (Q x))) (@imp A agA (@box A agA (@laterM A agA) (Q x)) (@box A agA (@laterM A agA) (P x)))))) (@fash A agA (@imp A agA (F y x (P (G y x))) (F y x (Q (G y x))))) *)
 eapply derives_trans; [ | apply eqp_subp; apply H].
(* Goal: @derives nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P x)) (@box A agA (@laterM A agA) (Q x))) (@imp A agA (@box A agA (@laterM A agA) (Q x)) (@box A agA (@laterM A agA) (P x)))))) (@box nat ag_nat (@laterM nat ag_nat) (@fash A agA (@andp A agA (@imp A agA (P (G y x)) (Q (G y x))) (@imp A agA (Q (G y x)) (P (G y x)))))) *)
 rewrite eqp_later.
(* Goal: @derives nat ag_nat (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) (@fash A agA (@andp A agA (@imp A agA (@box A agA (@laterM A agA) (P (G y x))) (@box A agA (@laterM A agA) (Q (G y x)))) (@imp A agA (@box A agA (@laterM A agA) (Q (G y x))) (@box A agA (@laterM A agA) (P (G y x)))))) *)
 apply allp_left with (G y x). auto.
Qed.
Lemma const_contractive {A}{agA: ageable A}: forall P : pred A, contractive (fun _ => P).
Proof.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
 intros.
(* Goal: forall (X Y : Type) (G : forall (_ : Y) (_ : X), X) (F : forall (_ : Y) (_ : X) (_ : @pred A agA), @pred A agA) (_ : forall (y : Y) (x : X), @contractive A agA (F y x)), @HOcontractive A agA X (fun (R : forall _ : X, @pred A agA) (x : X) => @exp A agA Y (fun y : Y => F y x (R (G y x)))) *)
 apply prove_contractive. intros. apply subp_refl.
Qed.
Lemma later_contractive' {A} `{ageable A} : contractive (box laterM).
Proof.
(* Goal: @contractive A H (@box A H (@laterM A H)) *)
  unfold contractive; intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
  apply subp_eqp.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  rewrite <- subp_later.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@imp A H Q P))) *)
  apply box_positive; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H P Q)) *)
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  apply eqp_subp; auto.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
  rewrite <- subp_later.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@imp A H Q P))) *)
  apply box_positive; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) (@fash A H (@imp A H Q P)) *)
  apply eqp_subp2; auto.
Qed.

End Trashcan.

