Require Import Setoid Morphisms RelationClasses Omega.
From ChargeCore.Logics Require Import ILogic ILInsts ILEmbed.

Set Implicit Arguments.
Unset Strict Implicit.
Set Maximal Implicit Insertion.

Section LaterSect.
  Context {A : Type}.
  Context `{ILOps: ILogicOps A}.

Class ILLOperators (A : Type) : Type := {
  illater : A -> A
}.

Class ILLater {ILLOps: ILLOperators A} : Type := {
  illogic :> ILogic A;
  spec_lob P : illater P |-- P -> |-- P;
  spec_later_weaken P : P |-- illater P;
  spec_later_impl P Q : illater (P -->> Q) -|- (illater P) -->> (illater Q);
  spec_later_forall {T} (F : T -> A) : illater (Forall x:T, F x) -|- Forall x:T, illater (F x);
  spec_later_exists {T} (F : T -> A) : Exists x : T, illater (F x) |-- illater (Exists x : T, F x);
  spec_later_exists_inhabited {T} (F : T -> A) : inhabited T -> illater (Exists x : T, F x) |-- Exists x : T, illater (F x)
}.
End LaterSect.

Arguments ILLater _ _ _ : clear implicits.
Arguments ILLater _ {ILLOps ILOps} : rename.
Notation "'|>' a"  := (illater a) (at level 71).

Section ILogicLaterCoreRules.
  Context {A} `{IL: ILLater A}.

  Global Instance spec_later_entails:
    Proper (lentails ==> lentails) illater.
  Proof.
(* Goal: @Proper (forall _ : A, A) (@respectful A A (@lequiv A ILOps) (@lequiv A ILOps)) (@illater A ILLOps) *)
    intros P P' HP.
(* Goal: @lentails A ILOps (@illater A ILLOps P) (@illater A ILLOps P') *)
    rewrite <- limplValid, <- spec_later_impl, <- spec_later_weaken, limplValid.
(* Goal: @lentails A ILOps P P' *)
    assumption.
  Qed.

  Global Instance spec_later_equiv:
    Proper (lequiv ==> lequiv) illater.
  Proof.
(* Goal: @Proper (forall _ : A, A) (@respectful A A (@lequiv A ILOps) (@lequiv A ILOps)) (@illater A ILLOps) *)
    intros P P' HP. split; cancel1; rewrite HP; reflexivity.
  Qed.

  Lemma spec_later_and P P': |>(P //\\ P') -|- |>P //\\ |>P'.
  Proof.
    do 2 rewrite land_is_forall; rewrite spec_later_forall;
    split; apply lforallR; intro x; apply lforallL with x;
(* Goal: @lentails A ILOps (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) *)
    destruct x; reflexivity.
  Qed.

  Lemma spec_later_or P P': |>(P \\// P') -|- |>P \\// |>P'.
  Proof.
    do 2 rewrite lor_is_exists; split;
    [rewrite spec_later_exists_inhabited; [|firstorder]| rewrite <- spec_later_exists];
(* Goal: @lentails A ILOps (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) *)
    apply lexistsL; intro x; apply lexistsR with x; destruct x; reflexivity.
  Qed.

  Lemma spec_later_true : |>ltrue -|- ltrue.
  Proof.
(* Goal: @lequiv A ILOps (@illater A ILLOps (@ltrue A ILOps)) (@ltrue A ILOps) *)
    split; [intuition|].
(* Goal: @lentails A ILOps (@ltrue A ILOps) (@illater A ILLOps (@ltrue A ILOps)) *)
    rewrite ltrue_is_forall, spec_later_forall.
(* Goal: @lentails A ILOps (@lforall A ILOps Empty_set (fun x : Empty_set => Empty_set_rect (fun _ : Empty_set => A) x)) (@lforall A ILOps Empty_set (fun x : Empty_set => @illater A ILLOps (Empty_set_rect (fun _ : Empty_set => A) x))) *)
    apply lforallR; intro x; destruct x.
  Qed.

End ILogicLaterCoreRules.

Hint Rewrite
  @spec_later_and
  @spec_later_impl
  @spec_later_true
  @spec_later_forall
  : push_later.

Section ILogic_nat.
  Context {A : Type}.
  Context `{IL: ILogic A}.

  Global Program Instance ILLaterNatOps : ILLOperators (ILPreFrm ge A)  :=
    {|
      illater P := mkILPreFrm (fun x => Forall y : nat, Forall H : y < x, (ILPreFrm_pred P) y) _
    |}.
  Next Obligation.
(* Goal: @lentails A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y t) (fun _ : lt y t => @ILPreFrm_pred nat ge A ILOps P y))) (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y t') (fun _ : lt y t' => @ILPreFrm_pred nat ge A ILOps P y))) *)
    intros.
(* Goal: @lentails A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y t) (fun _ : lt y t => @ILPreFrm_pred nat ge A ILOps P y))) (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y t') (fun _ : lt y t' => @ILPreFrm_pred nat ge A ILOps P y))) *)
    apply lforallR; intro x; apply lforallR; intro Hx; apply lforallL with x.
(* Goal: @lentails A ILOps (@lforall A ILOps (lt x t) (fun _ : lt x t => @ILPreFrm_pred nat ge A ILOps P x)) (@ILPreFrm_pred nat ge A ILOps P x) *)
    apply lforallL; [omega | reflexivity].
  Qed.

Local Transparent ILPre_Ops.

  Global Instance ILLaterNat : ILLater (ILPreFrm ge A).
  Proof.
(* Goal: @ILLater (Fun T A) (@ILFun_Ops T A ILOps) ILLaterFunOps *)
    split.
    + apply _.
    + intros P H x; induction x.
      - rewrite <- H; simpl; apply lforallR; intro y;
(* Goal: ge z a *)
(* Goal: @lentails A ILOps (@land A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (Init.Nat.add z (S O))) (fun _ : lt y (Init.Nat.add z (S O)) => @ILPreFrm_pred nat ge A ILOps Q y))) (@ILPreFrm_pred nat ge A ILOps P z)) (@ILPreFrm_pred nat ge A ILOps Q z) *)
        apply lforallR; intro Hy; omega.
      - rewrite <- H; simpl; apply lforallR; intro y; apply lforallR; intro Hy.
(* Goal: @lentails A ILOps (@ltrue A ILOps) (@ILPreFrm_pred nat ge A ILOps P y) *)
        assert (x >= y) by omega.
(* Goal: @lentails A ILOps P P' *)
        rewrite <- ILPreFrm_closed; eassumption.
    + intros P x; simpl; apply lforallR; intro y; apply lforallR; intro Hyx.
(* Goal: @lentails A ILOps (@ILPreFrm_pred nat ge A ILOps P x) (@ILPreFrm_pred nat ge A ILOps P y) *)
      apply ILPreFrm_closed; simpl. omega.
    + intros P Q; split; intros x; simpl.
      - apply lforallR; intro y; apply lforallR; intro Hxy.
(* Goal: @lentails A ILOps (@limpl A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (Init.Nat.add z (S O))) (fun _ : lt y (Init.Nat.add z (S O)) => @ILPreFrm_pred nat ge A ILOps P y))) (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (Init.Nat.add z (S O))) (fun _ : lt y (Init.Nat.add z (S O)) => @ILPreFrm_pred nat ge A ILOps Q y)))) (@limpl A ILOps (@ILPreFrm_pred nat ge A ILOps P z) (@ILPreFrm_pred nat ge A ILOps Q z)) *)
        apply limplAdj.
(* Goal: @lentails A ILOps (@land A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y x) (fun _ : lt y x => @lforall A ILOps nat (fun t' : nat => @lforall A ILOps (ge y t') (fun _ : ge y t' => @limpl A ILOps (@ILPreFrm_pred nat ge A ILOps P t') (@ILPreFrm_pred nat ge A ILOps Q t')))))) (@lforall A ILOps nat (fun y0 : nat => @lforall A ILOps (lt y0 y) (fun _ : lt y0 y => @ILPreFrm_pred nat ge A ILOps P y0)))) (@lforall A ILOps nat (fun y0 : nat => @lforall A ILOps (lt y0 y) (fun _ : lt y0 y => @ILPreFrm_pred nat ge A ILOps Q y0))) *)
        apply lforallR; intro z; apply lforallR; intro Hzy.
(* Goal: @lentails A ILOps (@land A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y x) (fun _ : lt y x => @lforall A ILOps nat (fun t' : nat => @lforall A ILOps (ge y t') (fun _ : ge y t' => @limpl A ILOps (@ILPreFrm_pred nat ge A ILOps P t') (@ILPreFrm_pred nat ge A ILOps Q t')))))) (@lforall A ILOps nat (fun y0 : nat => @lforall A ILOps (lt y0 y) (fun _ : lt y0 y => @ILPreFrm_pred nat ge A ILOps P y0)))) (@ILPreFrm_pred nat ge A ILOps Q z) *)
        rewrite landC, landforallD; [|apply _].
(* Goal: @lentails A ILOps (@lforall A ILOps nat (fun t' : nat => @lforall A ILOps (ge z t') (fun _ : ge z t' => @limpl A ILOps (@ILPreFrm_pred nat ge A ILOps P t') (@ILPreFrm_pred nat ge A ILOps Q t')))) (@limpl A ILOps (@ILPreFrm_pred nat ge A ILOps P z) (@ILPreFrm_pred nat ge A ILOps Q z)) *)
        apply lforallL with z.
(* Goal: @lentails A ILOps (@land A ILOps (@lforall A ILOps (lt z y) (fun _ : lt z y => @ILPreFrm_pred nat ge A ILOps P z)) (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y x) (fun _ : lt y x => @lforall A ILOps nat (fun t' : nat => @lforall A ILOps (ge y t') (fun _ : ge y t' => @limpl A ILOps (@ILPreFrm_pred nat ge A ILOps P t') (@ILPreFrm_pred nat ge A ILOps Q t'))))))) (@ILPreFrm_pred nat ge A ILOps Q z) *)
        rewrite landforallD; [|repeat split; assumption].
(* Goal: @lentails A ILOps (@lforall A ILOps (lt z y) (fun _ : lt z y => @land A ILOps (@ILPreFrm_pred nat ge A ILOps P z) (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y x) (fun _ : lt y x => @lforall A ILOps nat (fun t' : nat => @lforall A ILOps (ge y t') (fun _ : ge y t' => @limpl A ILOps (@ILPreFrm_pred nat ge A ILOps P t') (@ILPreFrm_pred nat ge A ILOps Q t')))))))) (@ILPreFrm_pred nat ge A ILOps Q z) *)
        apply lforallL with Hzy.
(* Goal: @lentails A ILOps (@land A ILOps (@ILPreFrm_pred nat ge A ILOps P z) (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y x) (fun _ : lt y x => @lforall A ILOps nat (fun t' : nat => @lforall A ILOps (ge y t') (fun _ : ge y t' => @limpl A ILOps (@ILPreFrm_pred nat ge A ILOps P t') (@ILPreFrm_pred nat ge A ILOps Q t'))))))) (@ILPreFrm_pred nat ge A ILOps Q z) *)
        rewrite landC. apply landAdj.
(* Goal: @lentails A ILOps (@lforall A ILOps nat (fun t' : nat => @lforall A ILOps (ge z t') (fun _ : ge z t' => @limpl A ILOps (@ILPreFrm_pred nat ge A ILOps P t') (@ILPreFrm_pred nat ge A ILOps Q t')))) (@limpl A ILOps (@ILPreFrm_pred nat ge A ILOps P z) (@ILPreFrm_pred nat ge A ILOps Q z)) *)
        apply lforallL with z. apply lforallL; [omega|].
(* Goal: @lentails A ILOps (@lforall A ILOps nat (fun t' : nat => @lforall A ILOps (ge z t') (fun _ : ge z t' => @limpl A ILOps (@ILPreFrm_pred nat ge A ILOps P t') (@ILPreFrm_pred nat ge A ILOps Q t')))) (@limpl A ILOps (@ILPreFrm_pred nat ge A ILOps P z) (@ILPreFrm_pred nat ge A ILOps Q z)) *)
        apply lforallL with z. apply lforallL; [omega|].
(* Goal: @lentails A ILOps (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) *)
	    reflexivity.
      - apply lforallR; intro y; apply lforallR; intro Hyx; apply lforallR; intro z; apply lforallR; intro Hyz.
        apply lforallL with (z + 1).
(* Goal: ge z a *)
(* Goal: @lentails A ILOps (@land A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (Init.Nat.add z (S O))) (fun _ : lt y (Init.Nat.add z (S O)) => @ILPreFrm_pred nat ge A ILOps Q y))) (@ILPreFrm_pred nat ge A ILOps P z)) (@ILPreFrm_pred nat ge A ILOps Q z) *)
        apply lforallL. omega.
(* Goal: @lentails A ILOps (@limpl A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (Init.Nat.add z (S O))) (fun _ : lt y (Init.Nat.add z (S O)) => @ILPreFrm_pred nat ge A ILOps P y))) (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (Init.Nat.add z (S O))) (fun _ : lt y (Init.Nat.add z (S O)) => @ILPreFrm_pred nat ge A ILOps Q y)))) (@limpl A ILOps (@ILPreFrm_pred nat ge A ILOps P z) (@ILPreFrm_pred nat ge A ILOps Q z)) *)
        apply limplAdj.
(* Goal: @lentails A ILOps (@land A ILOps (@limpl A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (Init.Nat.add z (S O))) (fun _ : lt y (Init.Nat.add z (S O)) => @ILPreFrm_pred nat ge A ILOps P y))) (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (Init.Nat.add z (S O))) (fun _ : lt y (Init.Nat.add z (S O)) => @ILPreFrm_pred nat ge A ILOps Q y)))) (@ILPreFrm_pred nat ge A ILOps P z)) (@ILPreFrm_pred nat ge A ILOps Q z) *)
        apply limplL.
(* Goal: @lentails A ILOps (@ILPreFrm_pred nat ge A ILOps P z) (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (Init.Nat.add z (S O))) (fun _ : lt y (Init.Nat.add z (S O)) => @ILPreFrm_pred nat ge A ILOps P y))) *)
(* Goal: @lentails A ILOps (@land A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (Init.Nat.add z (S O))) (fun _ : lt y (Init.Nat.add z (S O)) => @ILPreFrm_pred nat ge A ILOps Q y))) (@ILPreFrm_pred nat ge A ILOps P z)) (@ILPreFrm_pred nat ge A ILOps Q z) *)
        apply lforallR; intro a; apply lforallR; intro Ha.
(* Goal: ge z a *)
(* Goal: @lentails A ILOps (@land A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (Init.Nat.add z (S O))) (fun _ : lt y (Init.Nat.add z (S O)) => @ILPreFrm_pred nat ge A ILOps Q y))) (@ILPreFrm_pred nat ge A ILOps P z)) (@ILPreFrm_pred nat ge A ILOps Q z) *)
        apply ILPreFrm_closed. omega.
(* Goal: @lentails A ILOps (@land A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (Init.Nat.add z (S O))) (fun _ : lt y (Init.Nat.add z (S O)) => @ILPreFrm_pred nat ge A ILOps Q y))) (@ILPreFrm_pred nat ge A ILOps P z)) (@ILPreFrm_pred nat ge A ILOps Q z) *)
        apply landL1.
(* Goal: @lentails A ILOps (@lforall A ILOps (lt x t) (fun _ : lt x t => @ILPreFrm_pred nat ge A ILOps P x)) (@ILPreFrm_pred nat ge A ILOps P x) *)
        apply lforallL with z; apply lforallL; [omega | reflexivity].
    + intros T F; split; simpl; intros x.
      - apply lforallR; intro a; apply lforallR; intro y; apply lforallR; intro Hyx.
(* Goal: @lentails A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y x) (fun _ : lt y x => @lforall A ILOps T (fun a : T => @ILPreFrm_pred nat ge A ILOps (F a) y)))) (@ILPreFrm_pred nat ge A ILOps (F a) y) *)
        apply lforallL with y; apply lforallL with Hyx; apply lforallL with a.
(* Goal: @lentails A ILOps (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) *)
        reflexivity.
      - apply lforallR; intro y; apply lforallR; intro Hyx; apply lforallR; intro a.
(* Goal: @lentails A ILOps (@lforall A ILOps T (fun a : T => @lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y x) (fun _ : lt y x => @ILPreFrm_pred nat ge A ILOps (F a) y)))) (@ILPreFrm_pred nat ge A ILOps (F a) y) *)
        apply lforallL with a; apply lforallL with y; apply lforallL with Hyx.
(* Goal: @lentails A ILOps (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) *)
        reflexivity.
    + intros T F x; simpl.
(* Goal: @lentails A ILOps (@lexists A ILOps T (fun a : T => @lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y x) (fun _ : lt y x => @ILPreFrm_pred nat ge A ILOps (F a) y)))) (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y x) (fun _ : lt y x => @lexists A ILOps T (fun a : T => @ILPreFrm_pred nat ge A ILOps (F a) y)))) *)
      apply lexistsL; intro a; apply lforallR; intro y; apply lforallR; intro H.
(* Goal: @lentails A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y x) (fun _ : lt y x => @ILPreFrm_pred nat ge A ILOps (F a) y))) (@lexists A ILOps T (fun a : T => @ILPreFrm_pred nat ge A ILOps (F a) y)) *)
      apply lforallL with y; apply lforallL with H; apply lexistsR with a.
(* Goal: @lentails A ILOps (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) *)
      reflexivity.
    + intros T F Hin x; simpl.
(* Goal: @lentails A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y x) (fun _ : lt y x => @lexists A ILOps T (fun a : T => @ILPreFrm_pred nat ge A ILOps (F a) y)))) (@lexists A ILOps T (fun a : T => @lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y x) (fun _ : lt y x => @ILPreFrm_pred nat ge A ILOps (F a) y)))) *)
      inversion Hin as [a]; destruct x.
      - apply lexistsR with a; apply lforallR; intro y; apply lforallR; intro H; omega.
      - apply lforallL with x. apply lforallL; [omega|].
(* Goal: @lentails A ILOps (@lexists A ILOps T (fun a : T => @ILPreFrm_pred nat ge A ILOps (F a) x)) (@lexists A ILOps T (fun a : T => @lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (S x)) (fun _ : lt y (S x) => @ILPreFrm_pred nat ge A ILOps (F a) y)))) *)
        apply lexistsL; intro b; apply lexistsR with b.
(* Goal: @lentails A ILOps (@ILPreFrm_pred nat ge A ILOps (F b) x) (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (S x)) (fun _ : lt y (S x) => @ILPreFrm_pred nat ge A ILOps (F b) y))) *)
        apply lforallR; intro y; apply lforallR; intro H.
(* Goal: ge z a *)
(* Goal: @lentails A ILOps (@land A ILOps (@lforall A ILOps nat (fun y : nat => @lforall A ILOps (lt y (Init.Nat.add z (S O))) (fun _ : lt y (Init.Nat.add z (S O)) => @ILPreFrm_pred nat ge A ILOps Q y))) (@ILPreFrm_pred nat ge A ILOps P z)) (@ILPreFrm_pred nat ge A ILOps Q z) *)
        apply ILPreFrm_closed; omega.
  Qed.

End ILogic_nat.

Section IBILPre.
  Context T (ord: relation T) {ord_Pre: PreOrder ord}.
  Context {A : Type} `{HBI: ILLater A}.
  Context {IL : ILogic A}.

  Local Existing Instance ILPre_Ops.
  Local Existing Instance ILPre_ILogic.

  Local Transparent ILPre_Ops.

  Global Program Instance ILLaterPreOps : ILLOperators (ILPreFrm ord A) := {|
    illater P := mkILPreFrm (fun t => |>((ILPreFrm_pred P) t)) _
  |}.
  Next Obligation.
(* Goal: @lentails A ILOps (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) *)
    rewrite H. reflexivity.
  Qed.

  Program Definition ILLaterPre : ILLater (ILPreFrm ord A).
  Proof.
(* Goal: @ILLater (Fun T A) (@ILFun_Ops T A ILOps) ILLaterFunOps *)
    split.
    + apply _.
    + intros P HP x. apply spec_lob. apply HP.
    + intros P x. apply spec_later_weaken.
    + intros P Q; split; intros x; simpl;
        setoid_rewrite <- spec_later_impl;
(* Goal: @lentails A ILOps (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) (@illater A ILLOps (@ILPreFrm_pred T ord A ILOps P t')) *)
        do 2 setoid_rewrite spec_later_forall; reflexivity.
    + intros B F; split; intros x; simpl; apply spec_later_forall.
    + intros B F x; simpl; apply spec_later_exists.
    + intros B F I x; simpl; apply spec_later_exists_inhabited; apply I.
  Qed.

  Global Existing Instance ILLaterPre.

End IBILPre.

Section IBILogic_Fun.
  Context (T: Type).
  Context {A : Type} `{ILL: ILLater A}.

  Local Existing Instance ILFun_Ops.
  Local Existing Instance ILFun_ILogic.

  Local Transparent ILFun_Ops.

  Program Instance ILLaterFunOps : ILLOperators (Fun T A) := {|
    illater P := fun t => |>(P t)
  |}.

  Program Definition ILLaterFun : ILLater (Fun T A).
  Proof.
(* Goal: @ILLater (Fun T A) (@ILFun_Ops T A ILOps) ILLaterFunOps *)
    split.
    + apply _.
    + intros P HP x. apply spec_lob. apply HP.
    + intros P x. apply spec_later_weaken.
    + intros P Q; split; intros x; simpl;
      apply spec_later_impl.
    + intros B F; split; intros x; simpl; apply spec_later_forall.
    + intros B F x; simpl; apply spec_later_exists.
    + intros B F I x; simpl; apply spec_later_exists_inhabited; apply I.
  Qed.

  Global Existing Instance ILLaterFun.

End IBILogic_Fun.

Global Opaque ILLaterPreOps.
Global Opaque ILLaterNatOps.
Global Opaque ILLaterFunOps.
