Require Import Coq.Sets.Ensembles.
Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Logic.ChoiceFacts.
Require Import Coq.Logic.ClassicalChoice.
Require Import Logic.lib.RelationPairs_ext.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.SeparationLogic.Model.SeparationAlgebra.
Require Import Logic.SeparationLogic.Model.OrderedSA.

(***********************************)
(* Separation Algebra Generators   *)
(***********************************)

Section trivialSA.
  Context {worlds: Type}.
  
  Definition trivial_Join: Join worlds:=  (fun a b c => False).

  Definition trivial_SA: @SeparationAlgebra worlds trivial_Join.
  Proof.
(* Goal: @SeparationAlgebra worlds trivial_Join *)
    constructor; intuition.
(* Goal: @join worlds equiv_Join m2 m1 m *)
    inversion H.
  Qed.

  (* Trivial algebra is upwards closed *)
  (* Trivial is NOT downwards closed *)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
  Definition trivial_uSA {R: Relation worlds}:
    @UpwardsClosedSeparationAlgebra worlds R (trivial_Join).
  Proof.
(* Goal: @UpwardsClosedSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    intros until m2; intros.
(* Goal: @join worlds equiv_Join m2 m1 m *)
    inversion H.
  Qed.

  (*Increasing*)
  Definition trivial_incrSA: @IncreasingSeparationAlgebra
                           worlds eq trivial_Join.
  Proof.
(* Goal: @UnitalSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    constructor; intros.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    hnf; intros.
(* Goal: @join worlds equiv_Join m2 m1 m *)
    inversion H.
  Qed.

  (*Trivial is NOT necessarily unital*)

  (*Trivial is NOT necessarily residual*)
  
End trivialSA.

Section unitSA.
  Definition unit_Join: Join unit:=  (fun _ _ _ => True).

  Definition unit_SA: @SeparationAlgebra unit unit_Join.
  Proof.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    constructor.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    + intros. constructor.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    + intros; exists tt; split; constructor.
  Qed.

  (* Unit algebra is upwards closed *)
  Definition unit_uSA:
    @UpwardsClosedSeparationAlgebra unit eq unit_Join.
  Proof.
(* Goal: @UpwardsClosedSeparationAlgebra unit (@eq unit) unit_Join *)
    intros; exists tt, tt; intuition.
    + destruct m1; reflexivity.
    + destruct m2; reflexivity.
  Qed.

  (* Unit algebra is downwards closed *)
  Definition unit_dSA:
    @DownwardsClosedSeparationAlgebra unit eq unit_Join.
  Proof.
(* Goal: @DownwardsClosedSeparationAlgebra unit (@eq unit) unit_Join *)
    intros; exists tt; intuition.
(* Goal: @Krelation unit (@eq unit) tt m *)
    destruct m; reflexivity.
  Qed.

  (*Increasing*)
  Instance unit_incrSA:
    @IncreasingSeparationAlgebra unit eq unit_Join.
  Proof.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    constructor; intros; hnf; intros.
(* Goal: @Krelation unit (@eq unit) n n' *)
    destruct n, n'; reflexivity.
  Qed.

  Instance unit_residual:
    @ResidualSeparationAlgebra unit eq unit_Join.
  Proof.
(* Goal: @UnitalSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    constructor; intros.
(* Goal: @ex unit (fun m : unit => @residue unit (@eq unit) unit_Join n m) *)
    exists tt; exists tt; split.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    + constructor.
    + destruct n; reflexivity.
  Qed.

  Definition unit_unital:
    @UnitalSeparationAlgebra unit eq unit_Join.
  Proof.
(* Goal: @UnitalSeparationAlgebra unit (@eq unit) unit_Join *)
    apply <- (@incr_unital_iff_residual unit eq (eq_preorder unit) unit_Join); auto.
    + apply unit_residual.
    + apply unit_incrSA.
  Qed.

End unitSA.


Section equivSA.
  Context {worlds: Type}.
  
  Definition equiv_Join: Join worlds:=  (fun a b c => a = c /\ b = c).

  Definition equiv_SA: @SeparationAlgebra worlds equiv_Join.
  Proof.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    constructor.
    + intros.
(* Goal: @join worlds equiv_Join m2 m1 m *)
      inversion H.
(* Goal: @join worlds equiv_Join m2 m1 m *)
      split; tauto.
    + intros.
(* Goal: @ex (prod A B) (fun myz : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) my mz myz) (@join (prod A B) (@prod_Join A B Join_A Join_B) mx myz mxyz)) *)
      simpl in *.
(* Goal: @ex (prod A B) (fun n1 : prod A B => @ex (prod A B) (fun n2 : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) n1 n2 n) (and (@Krelation (prod A B) (@RelProd A B R_A R_B) m1 n1) (@Krelation (prod A B) (@RelProd A B R_A R_B) m2 n2)))) *)
      destruct H, H0.
(* Goal: @ex worlds (fun myz : worlds => and (@join worlds equiv_Join my mz myz) (@join worlds equiv_Join mx myz mxyz)) *)
      subst mx my mxy mz.
(* Goal: @ex worlds (fun myz : worlds => and (@join worlds equiv_Join mxyz mxyz myz) (@join worlds equiv_Join mxyz myz mxyz)) *)
      exists mxyz; do 2 split; auto.
  Qed.

  (* Identity algebra is upwards closed *)
  (* Identity is NOT downwards closed *)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
  Definition identity_uSA {R: Relation worlds}:
    @UpwardsClosedSeparationAlgebra worlds R equiv_Join.
  Proof.
(* Goal: @UpwardsClosedSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    intros until m2; intros.
(* Goal: @ex worlds (fun n1 : worlds => @ex worlds (fun n2 : worlds => and (@join worlds equiv_Join n1 n2 n) (and (@Krelation worlds R m1 n1) (@Krelation worlds R m2 n2)))) *)
    destruct H; subst m1 m2.
(* Goal: @ex worlds (fun n1 : worlds => @ex worlds (fun n2 : worlds => and (@join worlds equiv_Join n1 n2 n) (and (@Krelation worlds R m n1) (@Krelation worlds R m n2)))) *)
    exists n, n; do 2 split; auto.
  Qed.

  Definition equiv_incrSA: @IncreasingSeparationAlgebra
                           worlds eq equiv_Join.
  Proof.
(* Goal: @UnitalSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    constructor; intros.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    hnf; intros.
(* Goal: @increasing (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n0 *)
    inversion H; subst.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    constructor.
  Qed.

  Definition ikiM_uSA {R: Relation worlds} {po_R: PreOrder Krelation} {ikiM: IdentityKripkeIntuitionisticModel worlds} {J: Join worlds}: UpwardsClosedSeparationAlgebra worlds.
  Proof.
(* Goal: @UpwardsClosedSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    intros until m2; intros.
(* Goal: @ex worlds (fun n : worlds => and (@join worlds J n1 n2 n) (@Krelation worlds R n m)) *)
    apply Korder_identity in H0.
(* Goal: @ex worlds (fun n1 : worlds => @ex worlds (fun n2 : worlds => and (@join worlds J n1 n2 n) (and (@Krelation worlds R m1 n1) (@Krelation worlds R m2 n2)))) *)
    subst n.
(* Goal: @ex worlds (fun n1 : worlds => @ex worlds (fun n2 : worlds => and (@join worlds J n1 n2 m) (and (@Krelation worlds R m1 n1) (@Krelation worlds R m2 n2)))) *)
    exists m1, m2.
(* Goal: and (@join worlds J m1 m2 m) (and (@Krelation worlds R m1 m1) (@Krelation worlds R m2 m2)) *)
    split; [| split]; auto; reflexivity.
  Qed.

  Definition ikiM_dSA {R: Relation worlds} {po_R: PreOrder Krelation} {ikiM: IdentityKripkeIntuitionisticModel worlds} {J: Join worlds}: DownwardsClosedSeparationAlgebra worlds.
  Proof.
(* Goal: forall (a : A) (b : B) (_ : @increasing A R_A Join_A a) (_ : @increasing B R_B Join_B b), @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    intros until n2; intros.
(* Goal: @ex worlds (fun n : worlds => and (@join worlds J n1 n2 n) (@Krelation worlds R n m)) *)
    apply Korder_identity in H0.
(* Goal: @ex worlds (fun n : worlds => and (@join worlds J n1 n2 n) (@Krelation worlds R n m)) *)
    apply Korder_identity in H1.
(* Goal: @ex worlds (fun n : worlds => and (@join worlds J n1 n2 n) (@Krelation worlds R n m)) *)
    subst n1 n2.
(* Goal: @ex worlds (fun n : worlds => and (@join worlds J m1 m2 n) (@Krelation worlds R n m)) *)
    exists m.
(* Goal: and (@join worlds J m1 m2 m) (@Krelation worlds R m m) *)
    split; auto; reflexivity.
  Qed.

  (*Identity is NOT necessarily increasing*)

  (*Identity is NOT necessarily unital*)

  (*Identity is NOT necessarily residual*)
  
End equivSA.

Section optionSA.
  Context (worlds: Type).
  
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
  Inductive option_join {J: Join worlds}: option worlds -> option worlds -> option worlds -> Prop :=
  | None_None_join: option_join None None None
  | None_Some_join: forall a, option_join None (Some a) (Some a)
  | Some_None_join: forall a, option_join (Some a) None (Some a)
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
  | Some_Some_join: forall a b c, join a b c -> option_join (Some a) (Some b) (Some c).

(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
  Definition option_Join {SA: Join worlds}: Join (option worlds):=
    (@option_join SA).
  
  Definition option_SA
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
             {J: Join worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
             {SA: SeparationAlgebra worlds}:
    @SeparationAlgebra (option worlds) (option_Join).
  Proof.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    constructor.
    + intros.
(* Goal: @ex (prod A B) (fun myz : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) my mz myz) (@join (prod A B) (@prod_Join A B Join_A Join_B) mx myz mxyz)) *)
      simpl in *.
(* Goal: @join (option worlds) (@option_Join J) m2 m1 m *)
      destruct H.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - apply None_None_join.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - apply Some_None_join.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - apply None_Some_join.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - apply Some_Some_join.
(* Goal: @join B Join_B (m2 x) (m1 x) (m x) *)
      apply join_comm; auto.
      + intros.
(* Goal: @ex (prod A B) (fun myz : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) my mz myz) (@join (prod A B) (@prod_Join A B Join_A Join_B) mx myz mxyz)) *)
        simpl in *.
        inversion H; inversion H0; clear H H0; subst;
        try inversion H4; try inversion H5; try inversion H6; subst;
        try congruence;
        [.. | destruct (join_assoc _ _ _ _ _ H1 H5) as [? [? ?]];
           eexists; split; apply Some_Some_join; eassumption];
        eexists; split;
        try solve [ apply None_None_join | apply Some_None_join
                    | apply None_Some_join | apply Some_Some_join; eauto].
  Qed.

  (* Ordered option Upwards closed *)
  Lemma option_ord_uSA
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R: Relation worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J: Join worlds}
        (uSA: UpwardsClosedSeparationAlgebra worlds):
    @UpwardsClosedSeparationAlgebra (option worlds) (option01_relation Krelation) option_Join.
  Proof.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    hnf; intros.
(* Goal: @increasing (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n0 *)
    inversion H; subst.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - inversion H0; subst.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
      + exists None, None; repeat split; try constructor.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
      + exists (Some a), None; repeat split; try constructor.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - inversion H0; subst.
(* Goal: @ex (option worlds) (fun n1 : option worlds => @ex (option worlds) (fun n2 : option worlds => and (@join (option worlds) (@option_Join J) n1 n2 (@Some worlds b)) (and (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@None worlds) n1) (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@Some worlds a) n2)))) *)
      exists None, (Some b); repeat split; try constructor; auto.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - inversion H0; subst.
(* Goal: @ex (option worlds) (fun n1 : option worlds => @ex (option worlds) (fun n2 : option worlds => and (@join (option worlds) (@option_Join J) n1 n2 (@Some worlds b)) (and (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@Some worlds a) n1) (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@None worlds) n2)))) *)
      exists (Some b), None; repeat split; try constructor; auto.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - inversion H0; subst.
      destruct
        (uSA  _ _ _ _ H1 H3) as [n1 [n2 [HH1 [HH2 HH3]]]].
(* Goal: @ex (option worlds) (fun n1 : option worlds => @ex (option worlds) (fun n2 : option worlds => and (@join (option worlds) (@option_Join J) n1 n2 (@Some worlds b0)) (and (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@Some worlds a) n1) (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@Some worlds b) n2)))) *)
      exists (Some n1), (Some n2); repeat split; try constructor; auto.
  Qed.

  (* Downwards closed IF the algebra is increasing*)
  Lemma option_ord_dSA
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R: Relation worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {po_R: PreOrder Krelation}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J: Join worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {SA: SeparationAlgebra worlds}
        (dSA: DownwardsClosedSeparationAlgebra worlds)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {incrSA: IncreasingSeparationAlgebra worlds}:
    @DownwardsClosedSeparationAlgebra (option worlds) (option01_relation Krelation) option_Join.
  Proof.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    hnf; intros.
    inversion H0; [ | | inversion H1]; subst.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - exists n2; inversion H; subst; split; auto;
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
      destruct n2; constructor.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - exists n2; inversion H; subst; split; auto;
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
      destruct n2; constructor.
      + inversion H1.
      + inversion H; subst.
        apply all_increasing in H6.
        inversion H1; subst.
        transitivity b; auto.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    - exists (Some a); split; try constructor.
(* Goal: @Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@Some worlds a) m *)
      inversion H; subst; auto.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    - exists (Some a); split; try constructor.
      transitivity (Some b); auto.
(* Goal: @increasing (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n0 *)
      inversion H; subst.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
      constructor. eapply all_increasing. apply join_comm; eassumption.
(* Goal: @increasing (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n0 *)
    - inversion H; subst.
(* Goal: @ex (option worlds) (fun n : option worlds => and (@join (option worlds) (@option_Join J) (@Some worlds a) (@Some worlds a0) n) (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) n (@Some worlds c))) *)
      destruct (dSA _ _ _ _ _ H6 H2 H5) as [n [HH1 HH2]].
(* Goal: @ex (option worlds) (fun n : option worlds => and (@join (option worlds) (@option_Join J) (@Some worlds a) (@Some worlds a0) n) (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) n (@Some worlds c))) *)
      exists (Some n); split; constructor; auto.
  Qed.

  Lemma option_ord_incr_None
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R: Relation worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {po_R: PreOrder Krelation}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J: Join worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {SA: SeparationAlgebra worlds}:
    @increasing (option worlds) (option01_relation Krelation) option_Join None.
  Proof.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    hnf; intros.
(* Goal: @increasing (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n0 *)
    inversion H; subst.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    + constructor.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    + constructor.
(* Goal: @Krelation worlds R w w *)
      reflexivity.
  Qed.

  Lemma option_ord_res_None
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R: Relation worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {po_R: PreOrder Krelation}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J: Join worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {SA: SeparationAlgebra worlds}:
    forall n, @residue (option worlds) (option01_relation Krelation) option_Join n None.
  Proof.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    hnf; intros.
(* Goal: @residue (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n (@None worlds) *)
    exists n.
(* Goal: and (@residue (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n (@None worlds)) (@increasing' (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) (@None worlds)) *)
    split.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    + destruct n; constructor.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    + destruct n; constructor.
(* Goal: @Krelation worlds R w w *)
      reflexivity.
  Qed.

  Lemma option_ord_USA
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R: Relation worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {po_R: PreOrder Krelation}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J: Join worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {SA: SeparationAlgebra worlds}:
    @UnitalSeparationAlgebra (option worlds) (option01_relation Krelation) option_Join.
  Proof.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    constructor.
(* Goal: forall (a : A) (b : B) (_ : @increasing A R_A Join_A a) (_ : @increasing B R_B Join_B b), @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    intros.
(* Goal: @ex (option worlds) (fun m : option worlds => and (@residue (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n m) (@increasing' (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) m)) *)
    exists None.
(* Goal: and (@residue (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n (@None worlds)) (@increasing' (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) (@None worlds)) *)
    split.
    + apply option_ord_res_None.
    + apply option_ord_incr_None.
  Qed.

  (* Disjoint option Upwards closed*)
  Lemma option_disj_uSA
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R: Relation worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J: Join worlds}
        (uSA: UpwardsClosedSeparationAlgebra worlds):
    @UpwardsClosedSeparationAlgebra (option worlds) (option00_relation Krelation) option_Join.
  Proof.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    hnf; intros.
(* Goal: @increasing (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n0 *)
    inversion H; subst.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - inversion H0; subst.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
      exists None, None; repeat split; try constructor.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - inversion H0; subst.
(* Goal: @ex (option worlds) (fun n1 : option worlds => @ex (option worlds) (fun n2 : option worlds => and (@join (option worlds) (@option_Join J) n1 n2 (@Some worlds b)) (and (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@None worlds) n1) (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@Some worlds a) n2)))) *)
      exists None, (Some b); repeat split; try constructor; auto.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - inversion H0; subst.
(* Goal: @ex (option worlds) (fun n1 : option worlds => @ex (option worlds) (fun n2 : option worlds => and (@join (option worlds) (@option_Join J) n1 n2 (@Some worlds b)) (and (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@Some worlds a) n1) (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@None worlds) n2)))) *)
      exists (Some b), None; repeat split; try constructor; auto.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - inversion H0; subst.
      destruct
        (uSA  _ _ _ _ H1 H3) as [n1 [n2 [HH1 [HH2 HH3]]]].
(* Goal: @ex (option worlds) (fun n1 : option worlds => @ex (option worlds) (fun n2 : option worlds => and (@join (option worlds) (@option_Join J) n1 n2 (@Some worlds b0)) (and (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@Some worlds a) n1) (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@Some worlds b) n2)))) *)
      exists (Some n1), (Some n2); repeat split; try constructor; auto.
  Qed.

  (* Disjointed option Downwards *)
  Lemma option_disj_dSA
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R: Relation worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J: Join worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {SA: SeparationAlgebra worlds}
        (dSA: DownwardsClosedSeparationAlgebra worlds):
    @DownwardsClosedSeparationAlgebra (option worlds) (option00_relation Krelation) option_Join.
  Proof.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    hnf; intros.
(* Goal: @ex (option worlds) (fun n : option worlds => and (@join (option worlds) (@option_Join J) n1 n2 n) (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) n m)) *)
    inversion H0; [ | inversion H1]; subst.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - exists n2; inversion H; subst; split; auto;
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
      destruct n2; constructor.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    - exists (Some a); split; try constructor.
(* Goal: @Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@Some worlds a) m *)
      inversion H; subst; auto.
(* Goal: @increasing (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n0 *)
    - inversion H; subst.
(* Goal: @ex (option worlds) (fun n : option worlds => and (@join (option worlds) (@option_Join J) (@Some worlds a) (@Some worlds a0) n) (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) n (@Some worlds c))) *)
      destruct (dSA _ _ _ _ _ H6 H2 H5) as [n [HH1 HH2]].
(* Goal: @ex (option worlds) (fun n : option worlds => and (@join (option worlds) (@option_Join J) (@Some worlds a) (@Some worlds a0) n) (@Krelation (option worlds) (@option00_relation worlds (@Krelation worlds R)) n (@Some worlds c))) *)
      exists (Some n); split; constructor; auto.
  Qed.

  Lemma option_disj_incr_None
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R: Relation worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {po_R: PreOrder Krelation}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J: Join worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {SA: SeparationAlgebra worlds}:
    @increasing (option worlds) (option00_relation Krelation) option_Join None.
  Proof.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    hnf; intros.
(* Goal: @increasing (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n0 *)
    inversion H; subst.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    + constructor.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    + constructor.
(* Goal: @Krelation worlds R w w *)
      reflexivity.
  Qed.

  Lemma option_disj_res_None
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R: Relation worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {po_R: PreOrder Krelation}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J: Join worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {SA: SeparationAlgebra worlds}:
    forall n, @residue (option worlds) (option00_relation Krelation) option_Join n None.
  Proof.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    hnf; intros.
(* Goal: @residue (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n (@None worlds) *)
    exists n.
(* Goal: and (@residue (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n (@None worlds)) (@increasing' (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) (@None worlds)) *)
    split.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    + destruct n; constructor.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    + destruct n; constructor.
(* Goal: @Krelation worlds R w w *)
      reflexivity.
  Qed.

  Lemma option_disj_USA
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R: Relation worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {po_R: PreOrder Krelation}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J: Join worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {SA: SeparationAlgebra worlds}:
    @UnitalSeparationAlgebra (option worlds) (option00_relation Krelation) option_Join.
  Proof.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    constructor.
(* Goal: forall (a : A) (b : B) (_ : @increasing A R_A Join_A a) (_ : @increasing B R_B Join_B b), @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    intros.
(* Goal: @ex (option worlds) (fun m : option worlds => and (@residue (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n m) (@increasing' (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) m)) *)
    exists None.
(* Goal: and (@residue (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n (@None worlds)) (@increasing' (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) (@None worlds)) *)
    split.
    + apply option_disj_res_None.
    + apply option_disj_incr_None.
  Qed.

  Lemma option_disj_USA'
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R: Relation worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {po_R: PreOrder Krelation}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J: Join worlds}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {SA: SeparationAlgebra worlds}:
    @UnitalSeparationAlgebra' (option worlds) (option00_relation Krelation) option_Join.
  Proof.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    constructor.
(* Goal: forall (a : A) (b : B) (_ : @increasing A R_A Join_A a) (_ : @increasing B R_B Join_B b), @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    intros.
(* Goal: @ex (option worlds) (fun m : option worlds => and (@residue (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n m) (@increasing' (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) m)) *)
    exists None.
(* Goal: and (@residue (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n (@None worlds)) (@increasing' (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) (@None worlds)) *)
    split.
    + apply option_disj_res_None.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    + hnf; intros.
(* Goal: @increasing (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n0 *)
      inversion H; subst.
(* Goal: @increasing (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) (@None worlds) *)
      apply option_disj_incr_None.
  Qed.

End optionSA.

Section exponentialSA.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
  Definition fun_Join (A B: Type) {J_B: Join B}: Join (A -> B) :=
    (fun a b c => forall x, join (a x) (b x) (c x)).

  Definition fun_SA
             (A B: Type)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
             {Join_B: Join B}
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
             {SA_B: SeparationAlgebra B}: @SeparationAlgebra (A -> B) (fun_Join A B).
  Proof.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    constructor.
    + intros.
(* Goal: @ex (prod A B) (fun myz : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) my mz myz) (@join (prod A B) (@prod_Join A B Join_A Join_B) mx myz mxyz)) *)
      simpl in *.
(* Goal: @join (forall _ : A, B) (@fun_Join A B Join_B) m2 m1 m *)
      intros x; specialize (H x).
(* Goal: @join B Join_B (m2 x) (m1 x) (m x) *)
      apply join_comm; auto.
    + intros.
(* Goal: @ex (prod A B) (fun myz : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) my mz myz) (@join (prod A B) (@prod_Join A B Join_A Join_B) mx myz mxyz)) *)
      simpl in *.
(* Goal: @ex (forall _ : A, B) (fun myz : forall _ : A, B => and (@join (forall _ : A, B) (@fun_Join A B Join_B) my mz myz) (@join (forall _ : A, B) (@fun_Join A B Join_B) mx myz mxyz)) *)
      destruct (choice (fun x fx => join (my x) (mz x) fx /\ join (mx x) fx (mxyz x) )) as [myz ?].
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - intros x; specialize (H x); specialize (H0 x).
(* Goal: @ex B (fun y : B => and (@join B Join_B (my x) (mz x) y) (@join B Join_B (mx x) y (mxyz x))) *)
      apply (join_assoc _ _ _ _ _ H H0); auto.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - exists myz; firstorder.
  Qed.

  (* Exponential is upwards closed *)
  Lemma fun_uSA 
        (A B: Type)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_B: Relation B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J_B: Join B}
        (uSA_B: UpwardsClosedSeparationAlgebra B):
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    @UpwardsClosedSeparationAlgebra (A -> B) (pointwise_relation A R_B) (fun_Join A B).
  Proof.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    hnf; intros.
(* Goal: @Krelation (forall _ : A, B) (@pointwise_relation A B R_B) n1 n' *)
    unfold join, fun_Join in H.
(* Goal: @ex (forall _ : A, B) (fun n : forall _ : A, B => and (@join (forall _ : A, B) (@fun_Join A B J_B) n1 n2 n) (@Krelation (forall _ : A, B) (@pointwise_relation A B R_B) n m)) *)
    unfold Krelation, pointwise_relation in H0.
    destruct (choice (fun x nn => join (fst nn) (snd nn) (n x) /\
                               Krelation (m1 x) (fst nn) /\
                               Krelation (m2 x) (snd nn)))
      as [nn H1].
(* Goal: forall x : A, @ex B (fun y : B => and (@join B J_B (n1 x) (n2 x) y) (@Krelation B R_B y (m x))) *)
(* Goal: @ex (forall _ : A, B) (fun n : forall _ : A, B => and (@join (forall _ : A, B) (@fun_Join A B J_B) n1 n2 n) (@Krelation (forall _ : A, B) (@pointwise_relation A B R_B) n m)) *)
    intros x.
    destruct (uSA_B (m x) (n x) (m1 x) (m2 x) (H x) (H0 x)) as [x1 [x2 ?]];
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
      exists (x1, x2); auto.
(* Goal: @ex (forall _ : A, B) (fun n1 : forall _ : A, B => @ex (forall _ : A, B) (fun n2 : forall _ : A, B => and (@join (forall _ : A, B) (@fun_Join A B J_B) n1 n2 n) (and (@Krelation (forall _ : A, B) (@pointwise_relation A B R_B) m1 n1) (@Krelation (forall _ : A, B) (@pointwise_relation A B R_B) m2 n2)))) *)
    exists (fun x => fst (nn x)), (fun x => snd (nn x)).
    simpl; repeat split; intros x; specialize (H1 x); destruct H1 as [H1 [H2 H3]];
    assumption.
  Qed.

  
  (* Exponential is downwards closed *)
  Lemma fun_dSA 
        (A B: Type)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_B: Relation B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J_B: Join B}
        (dSA_B: DownwardsClosedSeparationAlgebra B):
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    @DownwardsClosedSeparationAlgebra (A -> B) (pointwise_relation A R_B) (fun_Join A B).
  Proof.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    hnf; intros.
(* Goal: @Krelation (forall _ : A, B) (@pointwise_relation A B R_B) n1 n' *)
    unfold join, fun_Join in H.
(* Goal: @ex (forall _ : A, B) (fun n : forall _ : A, B => and (@join (forall _ : A, B) (@fun_Join A B J_B) n1 n2 n) (@Krelation (forall _ : A, B) (@pointwise_relation A B R_B) n m)) *)
    unfold Krelation, pointwise_relation in H0.
    destruct (choice (fun x n => join (n1 x) (n2 x) (n) /\
                               Krelation (n) (m x)))
      as [n H2].
(* Goal: forall x : A, @ex B (fun y : B => and (@join B J_B (n1 x) (n2 x) y) (@Krelation B R_B y (m x))) *)
(* Goal: @ex (forall _ : A, B) (fun n : forall _ : A, B => and (@join (forall _ : A, B) (@fun_Join A B J_B) n1 n2 n) (@Krelation (forall _ : A, B) (@pointwise_relation A B R_B) n m)) *)
    intros x.
(* Goal: @ex B (fun y : B => and (@join B J_B (n1 x) (n2 x) y) (@Krelation B R_B y (m x))) *)
(* Goal: @ex (forall _ : A, B) (fun n : forall _ : A, B => and (@join (forall _ : A, B) (@fun_Join A B J_B) n1 n2 n) (@Krelation (forall _ : A, B) (@pointwise_relation A B R_B) n m)) *)
    destruct (dSA_B (m1 x) (m2 x) (m x) (n1 x) (n2 x) (H x) (H0 x)) as [x1 [x2 ?]]; auto.
    + apply H1.
    + exists x1; auto.
    + exists n; split; hnf; intros x; specialize (H2 x); destruct H2; auto.
  Qed.

  (* Exponential is increasing *)
  Lemma fun_incrSA 
        (A B: Type)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_B: Relation B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J_B: Join B}
        (incr_B: IncreasingSeparationAlgebra B):
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    @IncreasingSeparationAlgebra (A -> B) (pointwise_relation A R_B) (fun_Join A B).
  Proof.
(* Goal: @UnitalSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    constructor; intros.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    hnf; intros.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    hnf; intros.
(* Goal: R_B (n a) (n' a) *)
    specialize (H a).
(* Goal: R_B (n a) (n' a) *)
    eapply all_increasing; eauto.
  Qed.

  (* Exponential is Unital*)
  Lemma fun_unitSA 
        (A B: Type)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_B: Relation B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J_B: Join B}
        (USA_B: UnitalSeparationAlgebra B):
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    @UnitalSeparationAlgebra (A -> B) (pointwise_relation A R_B) (fun_Join A B).
  Proof.
(* Goal: @UnitalSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    constructor; intros.
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
    destruct (choice (fun x mx => residue (n x) mx /\ increasing mx)) as [M HH].
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
    { intros;
      specialize (incr_exists (n x)); intros [y HH];
      exists y; auto. }
(* Goal: and (@residue (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n (@None worlds)) (@increasing' (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) (@None worlds)) *)
    exists M; split.
    + cut (forall x, residue (n x) (M x)).
(* Goal: forall (a : A) (b : B) (_ : @increasing A R_A Join_A a) (_ : @increasing B R_B Join_B b), @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
      - clear; unfold residue; intros.
(* Goal: @ex (forall _ : A, B) (fun n' : forall _ : A, B => and (@join (forall _ : A, B) (@fun_Join A B J_B) M n' n) (@Krelation (forall _ : A, B) (@pointwise_relation A B R_B) n n')) *)
        apply choice in H; destruct H as [n' H].
        exists n'; split; hnf; intros x;
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
        specialize (H x); destruct H; auto.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
      - intros x; specialize (HH x); destruct HH; auto.
    + unfold increasing; intros.
(* Goal: @Krelation (forall _ : A, B) (@pointwise_relation A B R_B) n1 n' *)
      unfold join, fun_Join in H.
(* Goal: forall x : A, @ex B (fun y : B => and (@join B J_B (n1 x) (n2 x) y) (@Krelation B R_B y (m x))) *)
(* Goal: @ex (forall _ : A, B) (fun n : forall _ : A, B => and (@join (forall _ : A, B) (@fun_Join A B J_B) n1 n2 n) (@Krelation (forall _ : A, B) (@pointwise_relation A B R_B) n m)) *)
      hnf; intros x.
(* Goal: R_B (n1 x) (n' x) *)
      specialize (HH x); destruct HH as [ _ HH].
(* Goal: R_B (n0 x) (n' x) *)
      apply HH.
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
      auto.
  Qed.

  (* Exponential is Unital' *)
  Lemma fun_unitSA' 
        (A B: Type)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_B: Relation B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {J_B: Join B}
        (USA'_B: UnitalSeparationAlgebra' B):
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    @UnitalSeparationAlgebra' (A -> B) (pointwise_relation A R_B) (fun_Join A B).
  Proof.
(* Goal: @UnitalSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    constructor; intros.
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
    destruct (choice (fun x mx => residue (n x) mx /\ increasing' mx)) as [M HH].
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
    { intros;
      specialize (incr'_exists (n x)); intros [y HH];
      exists y; auto. }
(* Goal: and (@residue (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n (@None worlds)) (@increasing' (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) (@None worlds)) *)
    exists M; split.
    + cut (forall x, residue (n x) (M x)).
(* Goal: forall (a : A) (b : B) (_ : @increasing A R_A Join_A a) (_ : @increasing B R_B Join_B b), @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
      - clear; unfold residue; intros.
(* Goal: @ex (forall _ : A, B) (fun n' : forall _ : A, B => and (@join (forall _ : A, B) (@fun_Join A B J_B) M n' n) (@Krelation (forall _ : A, B) (@pointwise_relation A B R_B) n n')) *)
        apply choice in H; destruct H as [n' H].
        exists n'; split; hnf; intros x;
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
        specialize (H x); destruct H; auto.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
      - intros x; specialize (HH x); destruct HH; auto.
    + unfold increasing', increasing; intros.
(* Goal: @Krelation (forall _ : A, B) (@pointwise_relation A B R_B) n1 n' *)
      unfold join, fun_Join in H.
(* Goal: forall x : A, @ex B (fun y : B => and (@join B J_B (n1 x) (n2 x) y) (@Krelation B R_B y (m x))) *)
(* Goal: @ex (forall _ : A, B) (fun n : forall _ : A, B => and (@join (forall _ : A, B) (@fun_Join A B J_B) n1 n2 n) (@Krelation (forall _ : A, B) (@pointwise_relation A B R_B) n m)) *)
      hnf; intros x.
(* Goal: R_B (n1 x) (n' x) *)
      specialize (HH x); destruct HH as [ _ HH].
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
      eapply (HH _); eauto.
(* Goal: @Krelation B R_B (M x) (n0 x) *)
      apply H.
  Qed.

End exponentialSA.

Section sumSA.

(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
  Inductive sum_worlds {worlds1 worlds2}: Type:
    Type:=
  | lw (w:worlds1): sum_worlds
  | rw (w:worlds2): sum_worlds.

(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
  Inductive sum_join {A B: Type} {J1: Join A} {J2: Join B}:
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    @sum_worlds A B ->
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    @sum_worlds A B ->
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    @sum_worlds A B-> Prop :=
  | left_join a b c:
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
      join a b c ->
      sum_join (lw a) (lw b) (lw c)
  | right_join a b c:
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
      join a b c ->
      sum_join (rw a) (rw b) (rw c).

(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
  Definition sum_Join (A B: Type) {Join_A: Join A} {Join_B: Join B}: Join (@sum_worlds A B) :=
    (@sum_join A B Join_A Join_B).

(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
  Definition sum_SA (A B: Type) {Join_A: Join A} {Join_B: Join B} {SA_A: SeparationAlgebra A} {SA_B: SeparationAlgebra B}: @SeparationAlgebra (@sum_worlds A B) (sum_Join A B).
  Proof.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    constructor.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - intros; inversion H;
(* Goal: @join B Join_B (m2 x) (m1 x) (m x) *)
      constructor; apply join_comm; auto.
(* Goal: forall (a : A) (b : B) (_ : @increasing A R_A Join_A a) (_ : @increasing B R_B Join_B b), @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    - intros.
      inversion H; subst;
      inversion H0;
      destruct (join_assoc _ _ _ _ _ H1 H3) as [myz [HH1 HH2]].
      + exists (lw myz); split; constructor; auto.
      + exists (rw myz); split; constructor; auto.
  Qed.

End sumSA.

Section productSA.

(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
  Definition prod_Join (A B: Type) {Join_A: Join A} {Join_B: Join B}: Join (A * B) :=
    (fun a b c => join (fst a) (fst b) (fst c) /\ join (snd a) (snd b) (snd c)).

(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
  Definition prod_SA (A B: Type) {Join_A: Join A} {Join_B: Join B} {SA_A: SeparationAlgebra A} {SA_B: SeparationAlgebra B}: @SeparationAlgebra (A * B) (prod_Join A B).
  Proof.
(* Goal: @SeparationAlgebra (prod A B) (@prod_Join A B Join_A Join_B) *)
    constructor.
    + intros.
(* Goal: @ex (prod A B) (fun myz : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) my mz myz) (@join (prod A B) (@prod_Join A B Join_A Join_B) mx myz mxyz)) *)
      simpl in *.
      destruct H; split;
(* Goal: @join B Join_B (m2 x) (m1 x) (m x) *)
      apply join_comm; auto.
    + intros.
(* Goal: @ex (prod A B) (fun myz : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) my mz myz) (@join (prod A B) (@prod_Join A B Join_A Join_B) mx myz mxyz)) *)
      simpl in *.
(* Goal: @ex (prod A B) (fun n1 : prod A B => @ex (prod A B) (fun n2 : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) n1 n2 n) (and (@Krelation (prod A B) (@RelProd A B R_A R_B) m1 n1) (@Krelation (prod A B) (@RelProd A B R_A R_B) m2 n2)))) *)
      destruct H, H0.
(* Goal: @ex (prod A B) (fun myz : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) my mz myz) (@join (prod A B) (@prod_Join A B Join_A Join_B) mx myz mxyz)) *)
      destruct (join_assoc _ _ _ _ _ H H0) as [myz1 [? ?]].
(* Goal: @ex (prod A B) (fun myz : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) my mz myz) (@join (prod A B) (@prod_Join A B Join_A Join_B) mx myz mxyz)) *)
      destruct (join_assoc _ _ _ _ _ H1 H2) as [myz2 [? ?]].
(* Goal: @ex (prod A B) (fun myz : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) my mz myz) (@join (prod A B) (@prod_Join A B Join_A Join_B) mx myz mxyz)) *)
      exists (myz1, myz2).
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
      do 2 split; auto.
  Qed.

  Lemma prod_uSA
        (A B: Type)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_A: Relation A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_B: Relation B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {Join_A: Join A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {Join_B: Join B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {dSA_A: UpwardsClosedSeparationAlgebra A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {dSA_B: UpwardsClosedSeparationAlgebra B}:
    @UpwardsClosedSeparationAlgebra (A * B) (RelProd R_A R_B) (@prod_Join _ _ Join_A Join_B).
  Proof.
(* Goal: @UpwardsClosedSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    intros until m2; intros.
(* Goal: @ex (prod A B) (fun n1 : prod A B => @ex (prod A B) (fun n2 : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) n1 n2 n) (and (@Krelation (prod A B) (@RelProd A B R_A R_B) m1 n1) (@Krelation (prod A B) (@RelProd A B R_A R_B) m2 n2)))) *)
    destruct H, H0.
(* Goal: @ex (prod A B) (fun n1 : prod A B => @ex (prod A B) (fun n2 : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) n1 n2 n) (and (@Krelation (prod A B) (@RelProd A B R_A R_B) m1 n1) (@Krelation (prod A B) (@RelProd A B R_A R_B) m2 n2)))) *)
    destruct (join_Korder_up _ _ _ _ H H0) as [fst_n1 [fst_n2 [? [? ?]]]].
(* Goal: @ex (prod A B) (fun n1 : prod A B => @ex (prod A B) (fun n2 : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) n1 n2 n) (and (@Krelation (prod A B) (@RelProd A B R_A R_B) m1 n1) (@Krelation (prod A B) (@RelProd A B R_A R_B) m2 n2)))) *)
    destruct (join_Korder_up _ _ _ _ H1 H2) as [snd_n1 [snd_n2 [? [? ?]]]].
(* Goal: @ex (prod A B) (fun n1 : prod A B => @ex (prod A B) (fun n2 : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) n1 n2 n) (and (@Krelation (prod A B) (@RelProd A B R_A R_B) m1 n1) (@Krelation (prod A B) (@RelProd A B R_A R_B) m2 n2)))) *)
    exists (fst_n1, snd_n1), (fst_n2, snd_n2).
    do 2 split; simpl; auto;
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
    constructor; auto.
  Qed.

  Lemma prod_dSA
        (A B: Type)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_A: Relation A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_B: Relation B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {Join_A: Join A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {Join_B: Join B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {uSA_A: DownwardsClosedSeparationAlgebra A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {uSA_B: DownwardsClosedSeparationAlgebra B}:
    @DownwardsClosedSeparationAlgebra (A * B) (RelProd R_A R_B) (@prod_Join _ _ Join_A Join_B).
  Proof.
(* Goal: forall (a : A) (b : B) (_ : @increasing A R_A Join_A a) (_ : @increasing B R_B Join_B b), @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    intros until n2; intros.
(* Goal: @ex (prod A B) (fun n : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) n1 n2 n) (@Krelation (prod A B) (@RelProd A B R_A R_B) n m)) *)
    destruct H, H0, H1.
(* Goal: @ex (prod A B) (fun n : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) n1 n2 n) (@Krelation (prod A B) (@RelProd A B R_A R_B) n m)) *)
    destruct (join_Korder_down _ _ _ _ _ H H0 H1) as [fst_n [? ?]].
(* Goal: @ex (prod A B) (fun n : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) n1 n2 n) (@Krelation (prod A B) (@RelProd A B R_A R_B) n m)) *)
    destruct (join_Korder_down _ _ _ _ _ H2 H3 H4) as [snd_n [? ?]].
(* Goal: @ex (prod A B) (fun n : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) n1 n2 n) (@Krelation (prod A B) (@RelProd A B R_A R_B) n m)) *)
    exists (fst_n, snd_n).
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
    do 2 split; simpl; auto.
  Qed.

  Lemma prod_incr
        (A B: Type)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_A: Relation A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_B: Relation B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {Join_A: Join A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {Join_B: Join B}:
    forall (a: A) (b: B),
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
      increasing a -> increasing b ->
      @increasing _
                   (RelProd R_A R_B)
                   (@prod_Join _ _ Join_A Join_B) (a,b).
  Proof.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    intros. hnf; intros.
(* Goal: @Krelation (prod A B) (@RelProd A B R_A R_B) n n' *)
    destruct n, n'.
(* Goal: @ex (prod A B) (fun myz : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) my mz myz) (@join (prod A B) (@prod_Join A B Join_A Join_B) mx myz mxyz)) *)
    inversion H1; simpl in *.
(* Goal: and (@residue (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) n (@None worlds)) (@increasing' (option worlds) (@option00_relation worlds (@Krelation worlds R)) (@option_Join J) (@None worlds)) *)
    hnf; intros; split.
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
    apply H; auto.
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
    apply H0; auto.
  Qed.

  Lemma prod_incrSA
        (A B: Type)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_A: Relation A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_B: Relation B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {Join_A: Join A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {Join_B: Join B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {incrSA_A: IncreasingSeparationAlgebra A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {incrSA_B: IncreasingSeparationAlgebra B}:
    @IncreasingSeparationAlgebra (A * B) (RelProd R_A R_B) (@prod_Join _ _ Join_A Join_B).
  Proof.
(* Goal: @UnitalSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    constructor; intros.
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
    destruct x; apply prod_incr; auto.
    + apply incrSA_A.
    + apply incrSA_B.
  Qed.

  Lemma prod_residualSA
        (A B: Type)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_A: Relation A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_B: Relation B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {Join_A: Join A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {Join_B: Join B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {residualSA_A: ResidualSeparationAlgebra A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {residualSA_B: ResidualSeparationAlgebra B}:
    @ResidualSeparationAlgebra (A * B) (RelProd R_A R_B) (@prod_Join _ _ Join_A Join_B).
  Proof.
(* Goal: @UnitalSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    constructor; intros.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    destruct n as [a b].
    inversion residualSA_A;
      inversion residualSA_B.
(* Goal: @ex (prod A B) (fun m : prod A B => @residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) m) *)
    destruct (residue_exists a) as [a' [a'' [Ha1 Ha2]]].
(* Goal: @ex (prod A B) (fun m : prod A B => @residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) m) *)
    destruct (residue_exists0 b) as [b' [b'' [Hb1 Hb2]]].
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
    exists (a', b'); hnf; intros.
    exists (a'', b''); hnf; intros;
    split; hnf; intros;
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
    split; simpl; auto.
  Qed.

  Lemma prod_unitalSA
        (A B: Type)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_A: Relation A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {R_B: Relation B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {Join_A: Join A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {Join_B: Join B}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {unitalSA_A: UnitalSeparationAlgebra A}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
        {unitalSA_B: UnitalSeparationAlgebra B}:
    @UnitalSeparationAlgebra (A * B) (RelProd R_A R_B) (@prod_Join _ _ Join_A Join_B).
  Proof.
(* Goal: @UnitalSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    inversion unitalSA_A.
(* Goal: @UnitalSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    inversion unitalSA_B.
(* Goal: @UnitalSeparationAlgebra (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) *)
    constructor; intros.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
    - destruct n as [a b].
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
      destruct (incr_exists a) as [a' [Ha1 Ha2]].
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
      destruct (incr_exists0 b) as [b' [Hb1 Hb2]].
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
      exists (a', b'); split; hnf; intros.
      + destruct Ha1 as [a'' [Ha1 Ha3]].
(* Goal: @ex (prod A B) (fun n' : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) (@pair A B a' b') n' (@pair A B a b)) (@Krelation (prod A B) (@RelProd A B R_A R_B) (@pair A B a b) n')) *)
        destruct Hb1 as [b'' [Hb1 Hb3]].
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
        exists (a'',b''); split; hnf; hnf; intros; try constructor; simpl; auto.
      + destruct n, n'.
(* Goal: @ex (prod A B) (fun myz : prod A B => and (@join (prod A B) (@prod_Join A B Join_A Join_B) my mz myz) (@join (prod A B) (@prod_Join A B Join_A Join_B) mx myz mxyz)) *)
        inversion H; simpl in *.
(* Goal: @Krelation (prod A B) (@RelProd A B R_A R_B) (@pair A B a0 b0) (@pair A B a1 b1) *)
        apply Ha2 in H0.
(* Goal: @Krelation (prod A B) (@RelProd A B R_A R_B) (@pair A B a0 b0) (@pair A B a1 b1) *)
        apply Hb2 in H1.
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
        split; auto.
  Qed.

End productSA.

(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
Class SeparationAlgebra_unit (worlds: Type) {J: Join worlds} := {
                                                                 unit: worlds;
                                                                 unit_join: forall n, join n unit n;
(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
                                                                 unit_spec: forall n m, join n unit m -> n = m
                                                               }.

(***********************************)
(* Preorder examples               *)
(***********************************)


(***********************************)
(* dSA uSA examples                *)
(***********************************)


(***********************************)
(* More examples                   *)
(***********************************)

(*
Program Definition nat_le_kiM: KripkeIntuitionisticModel nat := 
  Build_KripkeIntuitionisticModel nat (fun a b => a <= b) _.
Next Obligation.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
  constructor; hnf; intros.
  + apply le_n.
  + eapply NPeano.Nat.le_trans; eauto.
Qed.

(* TODO: Probably don't need this one. *)
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
Program Definition SAu_kiM (worlds: Type) {J: Join worlds} {SA: SeparationAlgebra worlds} {SAu: SeparationAlgebra_unit worlds} : KripkeIntuitionisticModel worlds :=
  Build_KripkeIntuitionisticModel worlds (fun a b => exists b', join b b' a) _.
Next Obligation.
(* Goal: @increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) (@pair A B a b) *)
  constructor; hnf; intros.
  + exists unit; apply unit_join.
  + destruct H as [? ?], H0 as [? ?].
    destruct (join_assoc _ _ _ _ _ H0 H) as [? [? ?]].
(* Goal: @join B J_B (M x) (n0 x) (n' x) *)
    exists x2; auto.
Qed.

(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
Definition Heap (addr val: Type): Type := addr -> option val.

Instance Heap_Join (addr val: Type): Join (Heap addr val) :=
  @fun_Join _ _ (@option_Join _ (equiv_Join _)).

Instance Heap_SA (addr val: Type): SeparationAlgebra (Heap addr val) :=
  @fun_SA _ _ _ (@option_SA _ _ (equiv_SA _)).

Instance mfHeap_kiM (addr val: Type): KripkeIntuitionisticModel (Heap addr val) :=
  identity_kiM _.

Instance gcHeap_kiM (addr val: Type): KripkeIntuitionisticModel (Heap addr val) :=
  @fun_kiM _ _ (@option_ord_kiM _ (identity_kiM _)).

(* Goal: @ex (prod A B) (fun m : prod A B => and (@residue (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) n m) (@increasing (prod A B) (@RelProd A B R_A R_B) (@prod_Join A B Join_A Join_B) m)) *)
Definition Stack (LV val: Type): Type := LV -> val.

(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
Definition StepIndex_kiM (worlds: Type) {po_R: PreOrder Krelation}: KripkeIntuitionisticModel (nat * worlds) := @prod_kiM _ _ nat_le_kiM kiM.

(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
Definition StepIndex_Join (worlds: Type) {J: Join worlds}: Join (nat * worlds) :=
  @prod_Join _ _ (equiv_Join _) J.

(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
Definition StepIndex_SA (worlds: Type) {J: Join worlds} {SA: SeparationAlgebra worlds}:
  @SeparationAlgebra (nat * worlds) (StepIndex_Join worlds) := @prod_SA _ _ _ _ (equiv_SA _) SA.

(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
Definition StepIndex_dSA (worlds: Type) {po_R: PreOrder Krelation}
(* Goal: forall x : A, @ex B (fun y : B => and (@residue B R_B J_B (n x) y) (@increasing' B R_B J_B y)) *)
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@residue (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) n m) (@increasing' (forall _ : A, B) (@pointwise_relation A B R_B) (@fun_Join A B J_B) m)) *)
           {J: Join worlds} {dSA: UpwardsClosedSeparationAlgebra worlds}:
  @UpwardsClosedSeparationAlgebra (nat * worlds) (StepIndex_Join worlds) (StepIndex_kiM worlds):= @prod_dSA _ _ _ _ _ _ (@identity_dSA _ nat_le_kiM) dSA.

 *)