(*
 * Copyright (c) 2009-2010, Andrew Appel, Robert Dockins and Aquinas Hobor.
 *
 *)
Require Import VST.msl.base.
Require Import VST.msl.ageable.
Require Import VST.msl.sepalg.
Require Import VST.msl.sepalg_generators.

Class Age_alg (A:Type) {JOIN: Join A}{as_age : ageable A} :=
mkAge {
  age1_join : forall x {y z x'}, join x y z -> age x x' ->
    exists y':A, exists z':A, join x' y' z' /\ age y y' /\ age z z'
; age1_join2 : forall x {y z z'}, join x y z -> age z z' ->
    exists x':A, exists y':A, join x' y' z' /\ age x x' /\ age y y'
; unage_join : forall x {x' y' z'}, join x' y' z' -> age x x' ->
    exists y:A, exists z:A, join x y z /\ age y y' /\ age z z'
; unage_join2 : forall z {x' y' z'}, join x' y' z' -> age z z' ->
    exists x:A, exists y:A, join x y z /\ age x x' /\ age y y'
}.

Lemma age1_None_joins {A}{JA: Join A}{PA: Perm_alg A}{agA: ageable A}{XA: Age_alg A}: forall phi1 phi2, joins phi1 phi2 -> age1 phi1 = None -> age1 phi2 = None.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  destruct H.
(* Goal: @eq (option A) (@age1 A agA phi2) (@None A) *)
  case_eq (age1 phi2); intros; auto.
  destruct (age1_join _ (join_comm H) H1)  as [phi1' [x' [? [? ?]]]].
(* Goal: @eq (option A) (@Some A a) (@None A) *)
  unfold age in *; rewrite H0 in H3; inv H3.
Qed.

Lemma age1_joins_eq {A} {JA: Join A}{PA: Perm_alg A}{agA: ageable A}{XA: Age_alg A}: forall phi1 phi2,
        joins phi1 phi2 ->
        forall phi1', age1 phi1 = Some phi1' ->
        forall phi2', age1 phi2 = Some phi2' ->
        joins phi1' phi2'.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  destruct H.
(* Goal: @joins A JA phi1' phi2' *)
  destruct (age1_join _ H H0) as [phi7 [x' [? [? ?]]]].
(* Goal: @joins A JA phi1' phi2' *)
  unfold age in *; rewrite H1 in H3; inv H3.
(* Goal: @joins A JA phi1' phi7 *)
  exists x'; auto.
Qed.

Section BIJECTION.
  Variables A B : Type.
  Variable JA: Join A.
  Variable PA: Perm_alg A.
  Variable ag: ageable A.
  Variable bijAB: bijection A B.
  Variable asa : Age_alg A.

  Existing Instance PA.

  Instance agB : ageable B := (ag_bij _ _ ag bijAB).

(*  Instance PA_B:  @Perm_alg B (Join_bij _ _ _ bijAB ) := @Perm_bij A JA PA B bijAB. *)

  Theorem asa_bijection : @Age_alg B (Join_bij _ _ _ bijAB) agB.
  Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
    constructor; unfold age, Join_bij; simpl;     destruct bijAB as [f g fg gf]; simpl  in *; intros.

    (* commute1 *)
(* Goal: @ex B (fun y : B => @ex B (fun z : B => and (@join B (fun x y0 z0 : B => @join A JA (g x) (g y0) (g z0)) x y z) (and (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y')) (@eq (option B) match @age1 A ag (g z) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B z'))))) *)
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    revert H0; case_eq (age1 (g x)); intros; try discriminate.
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    inv H1.
(* Goal: @ex B (fun y : B => @ex B (fun z : B => and (@join B (fun x y0 z0 : B => @join A JA (g x) (g y0) (g z0)) x y z) (and (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y')) (@eq (option B) match @age1 A ag (g z) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B z'))))) *)
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    rename a into gx'.  red in H.
    destruct (age1_join _ H H0) as  [gy' [gz' [? [? ?]]]].
(* Goal: @ex B (fun y : B => @ex B (fun z : B => and (@join B (fun x y0 z0 : B => @join A JA (g x) (g y0) (g z0)) x y z) (and (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y')) (@eq (option B) match @age1 A ag (g z) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B z'))))) *)
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    exists (f gy'); exists (f gz').
(* Goal: and (@necR A agA y y) (@eq nat (@level A agA x') (@level A agA y)) *)
    split. red.
(* Goal: and (@eq (option B) match @age1 A ag (g (f gx')) with | Some y => @Some B (f y) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g (f gy')) with | Some y => @Some B (f y) | None => @None B end (@Some B y')) *)
    repeat rewrite gf. auto.
(* Goal: and (@eq (option B) match @age1 A ag gx' with | Some y => @Some B (f y) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag gy' with | Some y => @Some B (f y) | None => @None B end (@Some B y')) *)
    rewrite H2; rewrite H3.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    auto.

    (* commute2 *)
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    revert H0; case_eq (age1 (g z)); intros; try discriminate.
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    inv H1.
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    rename a into gz'. red in H.
    destruct (age1_join2 _ H H0) as  [gx' [gy' [? [? ?]]]].
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    exists (f gx'); exists (f gy').
(* Goal: and (@necR A agA y y) (@eq nat (@level A agA x') (@level A agA y)) *)
    split. red; repeat rewrite gf; auto.
(* Goal: and (@eq (option B) match @age1 A ag gx' with | Some y => @Some B (f y) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag gy' with | Some y => @Some B (f y) | None => @None B end (@Some B y')) *)
    rewrite H2; rewrite H3.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    auto.

    (* commute3 *)
(* Goal: @ex B (fun y : B => @ex B (fun z : B => and (@join B (fun x y0 z0 : B => @join A JA (g x) (g y0) (g z0)) x y z) (and (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y')) (@eq (option B) match @age1 A ag (g z) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B z'))))) *)
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    revert H0; case_eq (age1 (g x)); intros; try discriminate.
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    inv H1.
(* Goal: @ex B (fun y : B => @ex B (fun z : B => and (@join B (fun x y0 z0 : B => @join A JA (g x) (g y0) (g z0)) x y z) (and (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y')) (@eq (option B) match @age1 A ag (g z) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B z'))))) *)
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    rename a into gx'. red in H.
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    rewrite gf in *.
    destruct (unage_join _ H H0) as  [gy' [gz' [? [? ?]]]].
(* Goal: @ex B (fun y : B => @ex B (fun z : B => and (@join B (fun x y0 z0 : B => @join A JA (g x) (g y0) (g z0)) x y z) (and (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y')) (@eq (option B) match @age1 A ag (g z) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B z'))))) *)
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    exists (f gy'); exists (f gz').
(* Goal: and (@necR A agA y y) (@eq nat (@level A agA x') (@level A agA y)) *)
    split. red; repeat rewrite gf; auto.
(* Goal: and (@eq (option B) match @age1 A ag (g (f gx')) with | Some y => @Some B (f y) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g (f gy')) with | Some y => @Some B (f y) | None => @None B end (@Some B y')) *)
    repeat rewrite gf. rewrite H2; rewrite H3.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    repeat rewrite fg; split; auto.

    (* commute4 *)
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    revert H0; case_eq (age1 (g z)); intros; try discriminate.
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    inv H1.
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    rename a into gz'. red in H.
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    rewrite gf in *.
    destruct (unage_join2 _ H H0) as  [gx' [gy' [? [? ?]]]].
(* Goal: @ex B (fun x : B => @ex B (fun y : B => and (@join B (fun x0 y0 z : B => @join A JA (g x0) (g y0) (g z)) x y z) (and (@eq (option B) match @age1 A ag (g x) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g y) with | Some y0 => @Some B (f y0) | None => @None B end (@Some B y'))))) *)
    exists (f gx'); exists (f gy').
(* Goal: and (@necR A agA y y) (@eq nat (@level A agA x') (@level A agA y)) *)
    split. red.    repeat rewrite gf; auto.
(* Goal: and (@eq (option B) match @age1 A ag (g (f gx')) with | Some y => @Some B (f y) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag (g (f gy')) with | Some y => @Some B (f y) | None => @None B end (@Some B y')) *)
    repeat rewrite gf.
(* Goal: and (@eq (option B) match @age1 A ag gx' with | Some y => @Some B (f y) | None => @None B end (@Some B x')) (@eq (option B) match @age1 A ag gy' with | Some y => @Some B (f y) | None => @None B end (@Some B y')) *)
    rewrite H2; rewrite H3.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    repeat rewrite fg; split; auto.
  Qed.
End BIJECTION.

Section PROD.
  Variable A : Type.
  Variable J_A: Join A.
  Variable saA : Perm_alg A.
  Variable agA : ageable A.
  Variable B: Type.
  Variable J_B: Join B.
  Variable saB : Perm_alg B.
  Variable asa : Age_alg A.

  Theorem asa_prod : @Age_alg (prod A B) _ (ag_prod A B agA).
  Proof.
(* Goal: @Age_alg (prod A B) (Join_prod A J_A B J_B) (ag_prod' A B agB) *)
    constructor; unfold age; simpl; unfold Join_prod.

    (* commute1 *)
(* Goal: forall (x y z x' : prod A B) (_ : @join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')), @ex (prod A B) (fun y' : prod A B => @ex (prod A B) (fun z' : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x' y' z') (and (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y')) (@eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z'))))) *)
(* Goal: forall (x y z z' : prod A B) (_ : @join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x' : prod A B => @ex (prod A B) (fun y' : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x' y' z') (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
(* Goal: forall (x x' y' z' : prod A B) (_ : @join (prod A B) (fun x0 y z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y) (@snd A B z))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')), @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y')) (@eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z'))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    intros [xa xb] [ya yb] [za zb] [xa' xb'] [? ?].
(* Goal: forall _ : @eq (option (prod A B)) match @age1 B agB (@snd A B (@pair A B za zb)) with | Some a' => @Some (prod A B) (@pair A B (@fst A B (@pair A B za zb)) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za zb)) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    simpl in *.
(* Goal: forall _ : @eq (option (prod A B)) match @age1 A agA xa with | Some a' => @Some (prod A B) (@pair A B a' xb) | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb')), @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x y0 z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y0) (@snd A B z0))) (@pair A B xa xb) y z) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb'))) (@eq (option (prod A B)) match @age1 A agA (@fst A B z) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B z)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 A agA (@fst A B z) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B z)) | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B x) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B x)) | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    case_eq (age1 xa); intros; inv H2.
(* Goal: @ex (prod A B) (fun y' : prod A B => @ex (prod A B) (fun z' : prod A B => and (@join (prod A B) (fun x y z : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z))) (@pair A B xa' xb') y' z') (and (@eq (option (prod A B)) match @age1 A agA ya with | Some a' => @Some (prod A B) (@pair A B a' yb) | None => @None (prod A B) end (@Some (prod A B) y')) (@eq (option (prod A B)) match @age1 A agA za with | Some a' => @Some (prod A B) (@pair A B a' zb) | None => @None (prod A B) end (@Some (prod A B) z'))))) *)
(* Goal: forall (x y z z' : prod A B) (_ : @join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (_ : @eq (option (prod A B)) match @age1 A agA (@fst A B z) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B z)) | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x' : prod A B => @ex (prod A B) (fun y' : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x' y' z') (and (@eq (option (prod A B)) match @age1 A agA (@fst A B x) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B x)) | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
(* Goal: forall (x x' y' z' : prod A B) (_ : @join (prod A B) (fun x0 y z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y) (@snd A B z))) x' y' z') (_ : @eq (option (prod A B)) match @age1 A agA (@fst A B x) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B x)) | None => @None (prod A B) end (@Some (prod A B) x')), @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) y')) (@eq (option (prod A B)) match @age1 A agA (@fst A B z) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B z)) | None => @None (prod A B) end (@Some (prod A B) z'))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 A agA (@fst A B z) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B z)) | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B x) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B x)) | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    destruct (age1_join _ H H1) as [ya' [za' [? [? ?]]]].
    exists (ya',yb); exists (za',zb);
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
      rewrite H3; rewrite H4; repeat split; auto.

    (* commute2 *)
(* Goal: forall (x y z z' : prod A B) (_ : @join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x' : prod A B => @ex (prod A B) (fun y' : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x' y' z') (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
(* Goal: forall (x x' y' z' : prod A B) (_ : @join (prod A B) (fun x0 y z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y) (@snd A B z))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')), @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y')) (@eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z'))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    intros [xa xb] [ya yb] [za zb] [za' zb'] [? ?].
(* Goal: forall _ : @eq (option (prod A B)) match @age1 B agB (@snd A B (@pair A B za zb)) with | Some a' => @Some (prod A B) (@pair A B (@fst A B (@pair A B za zb)) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za zb)) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    simpl in *.
(* Goal: forall _ : @eq (option (prod A B)) match @age1 A agA za with | Some a' => @Some (prod A B) (@pair A B a' zb) | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za zb)) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B x) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B x)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    case_eq (age1 za); intros; inv H2.
(* Goal: @ex (prod A B) (fun x' : prod A B => @ex (prod A B) (fun y' : prod A B => and (@join (prod A B) (fun x y z : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z))) x' y' (@pair A B za' zb')) (and (@eq (option (prod A B)) match @age1 A agA xa with | Some a' => @Some (prod A B) (@pair A B a' xb) | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 A agA ya with | Some a' => @Some (prod A B) (@pair A B a' yb) | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
(* Goal: forall (x x' y' z' : prod A B) (_ : @join (prod A B) (fun x0 y z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y) (@snd A B z))) x' y' z') (_ : @eq (option (prod A B)) match @age1 A agA (@fst A B x) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B x)) | None => @None (prod A B) end (@Some (prod A B) x')), @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) y')) (@eq (option (prod A B)) match @age1 A agA (@fst A B z) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B z)) | None => @None (prod A B) end (@Some (prod A B) z'))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 A agA (@fst A B z) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B z)) | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B x) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B x)) | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    destruct (age1_join2 _ H H1) as [xa' [ya' [? [? ?]]]].
    exists (xa',xb); exists (ya',yb);
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
      rewrite H3; rewrite H4; repeat split; auto.

    (* commute3 *)
(* Goal: forall (x x' y' z' : prod A B) (_ : @join (prod A B) (fun x0 y z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y) (@snd A B z))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')), @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y')) (@eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z'))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    intros [xa xb] [xa' xb'] [ya' yb'] [za' zb'] [? ?].
(* Goal: forall _ : @eq (option (prod A B)) match @age1 B agB (@snd A B (@pair A B za zb)) with | Some a' => @Some (prod A B) (@pair A B (@fst A B (@pair A B za zb)) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za zb)) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    simpl in *.
(* Goal: forall _ : @eq (option (prod A B)) match @age1 A agA xa with | Some a' => @Some (prod A B) (@pair A B a' xb) | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb')), @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x y0 z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y0) (@snd A B z0))) (@pair A B xa xb) y z) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb'))) (@eq (option (prod A B)) match @age1 A agA (@fst A B z) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B z)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 A agA (@fst A B z) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B z)) | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B x) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B x)) | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    case_eq (age1 xa); intros; inv H2.
(* Goal: @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x y0 z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y0) (@snd A B z0))) (@pair A B xa xb') y z) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb'))) (@eq (option (prod A B)) match @age1 A agA (@fst A B z) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B z)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 A agA (@fst A B z) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B z)) | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B x) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B x)) | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    destruct (unage_join _ H H1) as [ya [za [? [? ?]]]].
(* Goal: @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x y0 z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y0) (@snd A B z0))) (@pair A B xa xb') y z) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb'))) (@eq (option (prod A B)) match @age1 A agA (@fst A B z) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B z)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 A agA (@fst A B z) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B z)) | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B x) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B x)) | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    exists (ya,yb'); exists (za,zb'); simpl.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    rewrite H3; rewrite H4; repeat split; auto.

    (* commute4 *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    intros [za zb] [xa' xb'] [ya' yb'] [za' zb'] [? ?].
(* Goal: forall _ : @eq (option (prod A B)) match @age1 B agB (@snd A B (@pair A B za zb)) with | Some a' => @Some (prod A B) (@pair A B (@fst A B (@pair A B za zb)) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za zb)) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    simpl in *.
(* Goal: forall _ : @eq (option (prod A B)) match @age1 A agA za with | Some a' => @Some (prod A B) (@pair A B a' zb) | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za zb)) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B x) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B x)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    case_eq (age1 za); intros; inv H2.
(* Goal: @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za zb')) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B x) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B x)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    destruct (unage_join2 _ H H1) as [xa [ya [? [? ?]]]].
(* Goal: @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za zb')) (and (@eq (option (prod A B)) match @age1 A agA (@fst A B x) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B x)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 A agA (@fst A B y) with | Some a' => @Some (prod A B) (@pair A B a' (@snd A B y)) | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    exists (xa,xb'); exists (ya,yb'); simpl.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    rewrite H3; rewrite H4; repeat split; auto.
  Qed.
End PROD.

Section PROD'.
  Variable A : Type.
  Variable J_A: Join A.
  Variable saA : Perm_alg A.
  Variable B: Type.
  Variable J_B: Join B.
  Variable saB : Perm_alg B.
  Variable agB : ageable B.
  Variable asb : Age_alg B.


  Theorem asa_prod' : @Age_alg (prod A B) _ (ag_prod' A B agB).
  Proof.
(* Goal: @Age_alg (prod A B) (Join_prod A J_A B J_B) (ag_prod' A B agB) *)
    constructor; unfold age; simpl; unfold Join_prod.

    (* commute1 *)
(* Goal: forall (x y z x' : prod A B) (_ : @join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')), @ex (prod A B) (fun y' : prod A B => @ex (prod A B) (fun z' : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x' y' z') (and (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y')) (@eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z'))))) *)
(* Goal: forall (x y z z' : prod A B) (_ : @join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x' : prod A B => @ex (prod A B) (fun y' : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x' y' z') (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
(* Goal: forall (x x' y' z' : prod A B) (_ : @join (prod A B) (fun x0 y z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y) (@snd A B z))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')), @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y')) (@eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z'))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    intros [xa xb] [ya yb] [za zb] [xa' xb'] [? ?].
(* Goal: forall _ : @eq (option (prod A B)) match @age1 B agB (@snd A B (@pair A B za zb)) with | Some a' => @Some (prod A B) (@pair A B (@fst A B (@pair A B za zb)) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za zb)) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    simpl in *.
(* Goal: forall _ : @eq (option (prod A B)) match @age1 B agB xb with | Some a' => @Some (prod A B) (@pair A B xa a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb')), @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x y0 z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y0) (@snd A B z0))) (@pair A B xa xb) y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    case_eq (age1 xb); intros; inv H2.
(* Goal: @ex (prod A B) (fun y' : prod A B => @ex (prod A B) (fun z' : prod A B => and (@join (prod A B) (fun x y z : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z))) (@pair A B xa' xb') y' z') (and (@eq (option (prod A B)) match @age1 B agB yb with | Some a' => @Some (prod A B) (@pair A B ya a') | None => @None (prod A B) end (@Some (prod A B) y')) (@eq (option (prod A B)) match @age1 B agB zb with | Some a' => @Some (prod A B) (@pair A B za a') | None => @None (prod A B) end (@Some (prod A B) z'))))) *)
(* Goal: forall (x y z z' : prod A B) (_ : @join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x' : prod A B => @ex (prod A B) (fun y' : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x' y' z') (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
(* Goal: forall (x x' y' z' : prod A B) (_ : @join (prod A B) (fun x0 y z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y) (@snd A B z))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')), @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y')) (@eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z'))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    destruct (age1_join _ H0 H1) as [yb' [zb' [? [? ?]]]].
    exists (ya,yb'); exists (za,zb');
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
      rewrite H3; rewrite H4; repeat split; auto.

    (* commute2 *)
(* Goal: forall (x y z z' : prod A B) (_ : @join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x' : prod A B => @ex (prod A B) (fun y' : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x' y' z') (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
(* Goal: forall (x x' y' z' : prod A B) (_ : @join (prod A B) (fun x0 y z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y) (@snd A B z))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')), @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y')) (@eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z'))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    intros [xa xb] [ya yb] [za zb] [za' zb'] [? ?].
(* Goal: forall _ : @eq (option (prod A B)) match @age1 B agB (@snd A B (@pair A B za zb)) with | Some a' => @Some (prod A B) (@pair A B (@fst A B (@pair A B za zb)) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za zb)) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    simpl in *.
(* Goal: forall _ : @eq (option (prod A B)) match @age1 B agB zb with | Some a' => @Some (prod A B) (@pair A B za a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za zb)) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    case_eq (age1 zb); intros; inv H2.
(* Goal: @ex (prod A B) (fun x' : prod A B => @ex (prod A B) (fun y' : prod A B => and (@join (prod A B) (fun x y z : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z))) x' y' (@pair A B za' zb')) (and (@eq (option (prod A B)) match @age1 B agB xb with | Some a' => @Some (prod A B) (@pair A B xa a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB yb with | Some a' => @Some (prod A B) (@pair A B ya a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
(* Goal: forall (x x' y' z' : prod A B) (_ : @join (prod A B) (fun x0 y z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y) (@snd A B z))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')), @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y')) (@eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z'))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    destruct (age1_join2 _ H0 H1) as [xb' [yb' [? [? ?]]]].
    exists (xa,xb'); exists (ya,yb');
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
      rewrite H3; rewrite H4; repeat split; auto.

    (* commute3 *)
(* Goal: forall (x x' y' z' : prod A B) (_ : @join (prod A B) (fun x0 y z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y) (@snd A B z))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')), @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y')) (@eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z'))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    intros [xa xb] [xa' xb'] [ya' yb'] [za' zb'] [? ?].
(* Goal: forall _ : @eq (option (prod A B)) match @age1 B agB (@snd A B (@pair A B za zb)) with | Some a' => @Some (prod A B) (@pair A B (@fst A B (@pair A B za zb)) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za zb)) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    simpl in *.
(* Goal: forall _ : @eq (option (prod A B)) match @age1 B agB xb with | Some a' => @Some (prod A B) (@pair A B xa a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb')), @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x y0 z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y0) (@snd A B z0))) (@pair A B xa xb) y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    case_eq (age1 xb); intros; inv H2.
(* Goal: @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x y0 z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y0) (@snd A B z0))) (@pair A B xa' xb) y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    destruct (unage_join _ H0 H1) as [yb [zb [? [? ?]]]].
(* Goal: @ex (prod A B) (fun y : prod A B => @ex (prod A B) (fun z : prod A B => and (@join (prod A B) (fun x y0 z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y0) (@snd A B z0))) (@pair A B xa' xb) y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')))))) *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    exists (ya',yb); exists (za',zb); simpl.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    rewrite H3; rewrite H4; repeat split; auto.

    (* commute4 *)
(* Goal: forall (z x' y' z' : prod A B) (_ : @join (prod A B) (fun x y z0 : prod A B => and (@join A J_A (@fst A B x) (@fst A B y) (@fst A B z0)) (@join B J_B (@snd A B x) (@snd A B y) (@snd A B z0))) x' y' z') (_ : @eq (option (prod A B)) match @age1 B agB (@snd A B z) with | Some a' => @Some (prod A B) (@pair A B (@fst A B z) a') | None => @None (prod A B) end (@Some (prod A B) z')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z0 : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z0)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z0))) x y z) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) x')) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) y'))))) *)
    intros [za zb] [xa' xb'] [ya' yb'] [za' zb'] [? ?].
(* Goal: forall _ : @eq (option (prod A B)) match @age1 B agB (@snd A B (@pair A B za zb)) with | Some a' => @Some (prod A B) (@pair A B (@fst A B (@pair A B za zb)) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za zb)) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    simpl in *.
(* Goal: forall _ : @eq (option (prod A B)) match @age1 B agB zb with | Some a' => @Some (prod A B) (@pair A B za a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B za' zb')), @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za zb)) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    case_eq (age1 zb); intros; inv H2.
(* Goal: @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za' zb)) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    destruct (unage_join2 _ H0 H1) as [xb [yb [? [? ?]]]].
(* Goal: @ex (prod A B) (fun x : prod A B => @ex (prod A B) (fun y : prod A B => and (@join (prod A B) (fun x0 y0 z : prod A B => and (@join A J_A (@fst A B x0) (@fst A B y0) (@fst A B z)) (@join B J_B (@snd A B x0) (@snd A B y0) (@snd A B z))) x y (@pair A B za' zb)) (and (@eq (option (prod A B)) match @age1 B agB (@snd A B x) with | Some a' => @Some (prod A B) (@pair A B (@fst A B x) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B xa' xb'))) (@eq (option (prod A B)) match @age1 B agB (@snd A B y) with | Some a' => @Some (prod A B) (@pair A B (@fst A B y) a') | None => @None (prod A B) end (@Some (prod A B) (@pair A B ya' yb')))))) *)
    exists (xa',xb); exists (ya',yb); simpl.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    rewrite H3; rewrite H4; repeat split; auto.
  Qed.
End PROD'.


Lemma joins_fashionR {A}  {JA: Join A}{PA: Perm_alg A}{agA: ageable A}{XA: Age_alg A} : forall x y,
  joins x y -> fashionR x y.
Proof.
(* Goal: forall (x y : A) (_ : @joins A JA x y), @fashionR A agA A agA x y *)
  pose proof I.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: @fashionR A agA A agA x y *)
  unfold fashionR.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  destruct H0 as [z ?].
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  revert y z H0; induction x using age_induction; intros.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  case_eq (age1 x); intros.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  destruct (age1_join _ H1 H2) as [p [q [? [? ?]]]].
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  assert (level a = level p).
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
  apply H0 with q; auto.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  replace (level x) with (S (level a)).
(* Goal: @eq nat (S (@level A agA a)) (@level A agA y) *)
(* Goal: @eq nat (S (@level A agA a)) (@level A agA x) *)
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  replace (level y) with (S (level p)).
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
  f_equal; auto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
  symmetry; apply age_level; auto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
  symmetry; apply age_level; auto.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  case_eq (age1 y); intros.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  apply join_comm in H1.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  destruct (age1_join _ H1 H3) as [p [q [? [? ?]]]].
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  hnf in H5; rewrite H5 in H2; discriminate.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  rewrite age1_level0 in H2.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  rewrite age1_level0 in H3.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  congruence.
Qed.

Lemma comparable_fashionR {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A} {agA: ageable A} {XA: Age_alg A} : forall x y,
  comparable x y -> fashionR x y.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: @fashionR A agA A agA x y *)
  apply comparable_common_unit in H.
(* Goal: @fashionR A agA A agA x y *)
  destruct H as [u [H1 H2]].
(* Goal: @fashionR A agA A agA x y *)
  hnf; transitivity (level u).
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
  apply joins_fashionR; eauto.
(* Goal: @eq nat (@level A agA u) (@level A agA y) *)
  symmetry.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
  apply joins_fashionR; eauto.
Qed.

Lemma age_identity {A} `{asaA: Age_alg A}: forall phi phi', age phi phi'->
    identity phi -> identity phi'.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
intros.
(* Goal: @identity A JOIN phi' *)
unfold identity in *.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
intros.
(* Goal: @eq A a b *)
destruct (unage_join _ H1 H) as [y [? [? [? ?]]]].
(* Goal: @eq A a b *)
specialize ( H0 y x H2).
(* Goal: @laterR A agA y y' *)
subst.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
unfold age in *. congruence.
Qed.

Lemma age_comparable {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A} {agA: ageable A}{asaA: Age_alg A}:
    forall phi1 phi2 phi1' phi2', age phi1 phi1' -> age phi2 phi2' ->
      comparable phi1 phi2 -> comparable phi1' phi2'.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: @comparable A JA SA phi1' phi2' *)
  destruct (comparable_common_unit H1) as [e [? ?]].
(* Goal: @comparable A JA SA phi1' phi2' *)
  destruct (age1_join _ (join_comm H2) H) as [a [b [? [? ?]]]].
(* Goal: @comparable A JA SA phi1' phi2' *)
  destruct (age1_join _ (join_comm H3) H0) as [c [d [? [? ?]]]].
(* Goal: @comparable A JA SA phi1' phi2' *)
  assert (c=a) by (unfold age in *; congruence); subst c.
(* Goal: @comparable A JA SA phi1' phi2' *)
  assert (b=phi1') by (unfold age in *; congruence). subst b.
(* Goal: @comparable A JA SA phi1' phi2' *)
  assert (d=phi2') by (unfold age in *; congruence). subst d.
(* Goal: @comparable A JA SA phi1' phi2' *)
  apply common_unit_comparable.
(* Goal: @ex A (fun y' : A => @relation_power A n (@age A agA) y y') *)
  exists a.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
  split; apply join_comm; auto.
Qed.

  Lemma asa_nat : @Age_alg nat (Join_equiv nat) ag_nat.
  Proof.
(* Goal: @Age_alg nat (Join_equiv nat) ag_nat *)
    constructor.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    repeat intro. hnf in H; subst; auto.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
    intros.
(* Goal: @laterR A agA y y' *)
    destruct H; subst.
(* Goal: @ex nat (fun z' : nat => and (@join nat (Join_equiv nat) x' x' z') (and (@age nat ag_nat z x') (@age nat ag_nat z z'))) *)
(* Goal: forall (x y z z' : nat) (_ : @join nat (Join_equiv nat) x y z) (_ : @age nat ag_nat z z'), @ex nat (fun x' : nat => @ex nat (fun y' : nat => and (@join nat (Join_equiv nat) x' y' z') (and (@age nat ag_nat x x') (@age nat ag_nat y y')))) *)
(* Goal: forall (x x' y' z' : nat) (_ : @join nat (Join_equiv nat) x' y' z') (_ : @age nat ag_nat x x'), @ex nat (fun y : nat => @ex nat (fun z : nat => and (@join nat (Join_equiv nat) x y z) (and (@age nat ag_nat y y') (@age nat ag_nat z z')))) *)
(* Goal: forall (z x' y' z' : nat) (_ : @join nat (Join_equiv nat) x' y' z') (_ : @age nat ag_nat z z'), @ex nat (fun x : nat => @ex nat (fun y : nat => and (@join nat (Join_equiv nat) x y z) (and (@age nat ag_nat x x') (@age nat ag_nat y y')))) *)
    exists x'. exists x'.
(* Goal: @eq nat (@level A agA (@core A JA SA m)) (@level A agA m) *)
    intuition.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
    intros.
(* Goal: @laterR A agA y y' *)
    destruct H; subst.
(* Goal: @eq nat (@level A agA (@core A JA SA m)) (@level A agA m) *)
    exists z'; exists z'; intuition.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
    intros. destruct H; subst.
(* Goal: @eq nat (@level A agA (@core A JA SA m)) (@level A agA m) *)
    exists x; exists x. intuition.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
    intros. destruct H; subst.
(* Goal: @eq nat (@level A agA (@core A JA SA m)) (@level A agA m) *)
    exists z; exists z; intuition.
  Qed.

Lemma nec_identity {A} `{asaA: Age_alg A}: forall phi phi', necR phi phi'->
    identity phi -> identity phi'.
Proof.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
  induction 1; auto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
  apply age_identity; auto.
Qed.

Lemma nec_join2 {A} `{asaA : Age_alg A}: forall {x y z z' : A},
       join x y z ->
       necR z z' ->
       exists x',
         exists y',
           join x' y' z' /\ necR x x' /\ necR y y'.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
intros.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
revert x y H; induction H0; intros.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
edestruct (age1_join2) as [x' [y' [? [? ?]]]]; eauto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
exists x'; exists y'; split; auto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
split; constructor 1; auto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
exists x0; exists y; split; auto.
(* Goal: @ex A (fun x' : A => @ex A (fun y' : A => and (@join A JOIN x' y' z) (and (@necR A as_age x0 x') (@necR A as_age y0 y')))) *)
destruct (IHclos_refl_trans1 _ _ H) as [x' [y' [? [? ?]]]].
(* Goal: @ex A (fun x' : A => @ex A (fun y' : A => and (@join A JOIN x' y' z) (and (@necR A as_age x0 x') (@necR A as_age y0 y')))) *)
destruct (IHclos_refl_trans2 _ _ H0) as [x'' [y'' [? [? ?]]]].
(* Goal: @ex A (fun x' : A => @ex A (fun y' : A => and (@join A JOIN x' y' z) (and (@necR A as_age x0 x') (@necR A as_age y0 y')))) *)
exists x''; exists y''.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
split; auto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
split; econstructor 3; eauto.
Qed.

Lemma nec_join {A} `{asaA : Age_alg A}: forall {x y z x' : A},
       join x y z ->
       necR x x' ->
       exists y' ,
         exists z' ,
           join x' y' z' /\ necR y y' /\ necR z z'.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
intros.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
revert y z H; induction H0; intros.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
edestruct age1_join as [y' [z' [? [? ?]]]]; eauto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
exists y'; exists z'; split; auto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
split; constructor 1; auto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
exists y; exists z; split; auto.
(* Goal: @ex A (fun y' : A => @ex A (fun z' : A => and (@join A JOIN z y' z') (and (@necR A as_age y0 y') (@necR A as_age z0 z')))) *)
destruct (IHclos_refl_trans1 _ _ H) as [y' [z' [? [? ?]]]].
(* Goal: @ex A (fun y' : A => @ex A (fun z' : A => and (@join A JOIN z y' z') (and (@necR A as_age y0 y') (@necR A as_age z0 z')))) *)
destruct (IHclos_refl_trans2 _ _ H0) as [y'' [z'' [? [? ?]]]].
(* Goal: @ex A (fun y' : A => @ex A (fun z' : A => and (@join A JOIN z y' z') (and (@necR A as_age y0 y') (@necR A as_age z0 z')))) *)
exists y''; exists z''.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
split; auto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
split; econstructor 3; eauto.
Qed.

Lemma nec_join4 {A} `{asaA : Age_alg A}: forall z x' y' z' : A,
       join x' y' z' ->
       necR z z' ->
       exists x,
         exists y,
           join x y z /\ necR x x' /\ necR y y'.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
intros.
(* Goal: @ex A (fun x : A => @ex A (fun y : A => and (@join A JOIN x y z) (and (@necR A as_age x x') (@necR A as_age y y')))) *)
revert x' y' H.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
induction H0; intros.
destruct (unage_join2 _ H0 H) as  [x0 [y0 [? [? ?]]]].
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
exists x0; exists y0; split; auto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
split; constructor 1; auto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
exists x'; exists y'; split; auto.

(* Goal: @ex A (fun x0 : A => @ex A (fun y : A => and (@join A JOIN x0 y x) (and (@necR A as_age x0 x') (@necR A as_age y y')))) *)
rename x into z1.
(* Goal: @ex A (fun x : A => @ex A (fun y : A => and (@join A JOIN x y z1) (and (@necR A as_age x x') (@necR A as_age y y')))) *)
rename y into z2.
(* Goal: @ex A (fun x : A => @ex A (fun y : A => and (@join A JOIN x y z1) (and (@necR A as_age x x') (@necR A as_age y y')))) *)
destruct (IHclos_refl_trans2 _ _ H) as [x'' [y'' [? [? ?]]]].
(* Goal: @ex A (fun x : A => @ex A (fun y : A => and (@join A JOIN x y z1) (and (@necR A as_age x x') (@necR A as_age y y')))) *)
destruct (IHclos_refl_trans1 _ _ H0) as [x0 [y0 [? [? ?]]]].
(* Goal: @ex A (fun x : A => @ex A (fun y : A => and (@join A JOIN x y z1) (and (@necR A as_age x x') (@necR A as_age y y')))) *)
exists x0; exists y0.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
split; auto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
split; econstructor 3; eauto.
Qed.


Lemma join_level {A}{JA: Join A}{PA: Perm_alg A}{AG: ageable A}{AgeA: Age_alg A}:
  forall x y z, join x y z -> level x = level z /\ level y = level z.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: and (@eq nat (@level A AG x) (@level A AG z)) (@eq nat (@level A AG y) (@level A AG z)) *)
  assert (exists n, n = level x) by (eexists; reflexivity).
  destruct H0 as [n  ?].
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  revert x y z H0 H; induction n; intros.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  case_eq (level y); intros.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  case_eq (level z); intros.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  split; congruence.
(* Goal: and (@eq nat (@level A AG x) (S n)) (@eq nat O (S n)) *)
(* Goal: and (@eq nat (@level A AG x) (@level A AG z)) (@eq nat (S n) (@level A AG z)) *)
(* Goal: and (@eq nat (@level A AG x) (@level A AG z)) (@eq nat (@level A AG y) (@level A AG z)) *)
  destruct (levelS_age1 _ _ H2).
(* Goal: and (@eq nat (@level A AG x) (S n)) (@eq nat O (S n)) *)
(* Goal: and (@eq nat (@level A AG x) (@level A AG z)) (@eq nat (S n) (@level A AG z)) *)
(* Goal: and (@eq nat (@level A AG x) (@level A AG z)) (@eq nat (@level A AG y) (@level A AG z)) *)
  destruct (age1_join2 _ H H3) as [u [v [? [? ?]]]].
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  apply age_level in H5. congruence.
(* Goal: and (@eq nat (@level A AG x) (@level A AG z)) (@eq nat (S n) (@level A AG z)) *)
(* Goal: and (@eq nat (@level A AG x) (@level A AG z)) (@eq nat (@level A AG y) (@level A AG z)) *)
  destruct (levelS_age1 _ _ H1).
(* Goal: and (@eq nat (@level A AG x) (@level A AG z)) (@eq nat (S n) (@level A AG z)) *)
(* Goal: and (@eq nat (@level A AG x) (@level A AG z)) (@eq nat (@level A AG y) (@level A AG z)) *)
  destruct (age1_join _ (join_comm H) H2) as [u [v [? [? ?]]]].
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  apply age_level in H4. congruence.
(* Goal: and (@eq nat (@level A AG x) (@level A AG z)) (@eq nat (@level A AG y) (@level A AG z)) *)
  symmetry in H0.
(* Goal: and (@eq nat (@level A AG x) (@level A AG z)) (@eq nat (@level A AG y) (@level A AG z)) *)
  destruct (levelS_age1 _ _ H0) as [x' ?].
(* Goal: and (@eq nat (@level A AG x) (@level A AG z)) (@eq nat (@level A AG y) (@level A AG z)) *)
  destruct (age1_join _ H H1) as [y' [z' [? [? ?]]]].
(* Goal: and (@eq nat (@level A AG x) (@level A AG z)) (@eq nat (@level A AG y) (@level A AG z)) *)
  specialize (IHn x' y' z').
(* Goal: and (@eq nat (@level A AG x) (@level A AG z)) (@eq nat (@level A AG y) (@level A AG z)) *)
  apply age_level in H1. apply age_level in H3. apply age_level in H4.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
  destruct IHn; auto. congruence.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  split; congruence.
Qed.

 Lemma level_core {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
     forall m:A, level (core m) = level m.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
 Proof. intros.
(* Goal: @eq nat (@level A agA (@core A JA SA m)) (@level A agA m) *)
  generalize (core_unit m); unfold unit_for; intro.
(* Goal: @eq nat (@level A agA (@core A JA SA m)) (@level A agA m) *)
  apply join_level in H. intuition.
 Qed.

Lemma age_core_eq {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall x y x' y', age x x' -> age y y' -> core x = core y -> core x' = core y'.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
 intros.
(* Goal: @eq A (@core A JA SA x') (@core A JA SA y') *)
 generalize (core_unit x); unfold unit_for; intro. apply join_comm in H2.
(* Goal: @eq A (@core A JA SA x') (@core A JA SA y') *)
 generalize (core_unit y); unfold unit_for; intro. apply join_comm in H3.
(* Goal: @eq A (@core A JA SA x') (@core A JA SA y') *)
 destruct (age1_join _ H2 H) as [u [v [? [? ?]]]].
(* Goal: @eq A (@core A JA SA x') (@core A JA SA y') *)
 destruct (age1_join _ H3 H0) as [i [j [? [? ?]]]].
(* Goal: @age A agA (@core A JA SA x) (@core A JA SA y) *)
 unfold age in *. rewrite H in H6. inv H6. rewrite H0 in H9; inv H9.
(* Goal: @eq A (@core A JA SA v) (@core A JA SA j) *)
 rewrite H1 in *. rewrite H5 in H8; inv H8.
(* Goal: @eq A (@core A JA SA v) (@core A JA SA j) *)
 apply join_core2 in H4. apply join_core2 in H7.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
  congruence.
Qed.

Lemma age_twin {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}:
  forall phi1 phi2 n phi1',
  level phi1 = level phi2 ->
  ageN n phi1 = Some phi1' ->
  exists phi2', ageN n phi2 = Some phi2' /\ level phi1' = level phi2'.
Proof.
(* Goal: forall (phi1 phi2 : A) (n : nat) (phi1' : A) (_ : @eq nat (@level A AG phi1) (@level A AG phi2)) (_ : @eq (option A) (@ageN A AG n phi1) (@Some A phi1')), @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG n phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
intros until n; revert n phi1 phi2.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
induction n; intros.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG O phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
exists phi2.
(* Goal: and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2')) *)
split; trivial.
(* Goal: @eq nat (@level A AG phi1') (@level A AG phi2) *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
inversion H0.
(* Goal: @eq nat (@level A AG phi1') (@level A AG phi2) *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
subst phi1'.
(* Goal: @eq (option A) (@composeOptN A (@age1 A AG) n ophi2) (@Some A phi2') *)
trivial.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
unfold ageN in H0.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
simpl in H0.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
revert H0; case_eq (age1 phi1); intros; try discriminate.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
rename a into phi.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
assert (exists ophi2, age phi2 ophi2 /\ level phi = level ophi2).
(* Goal: @ex A (fun ophi2 : A => and (@age A AG phi2 ophi2) (@eq nat (@level A AG phi) (@level A AG ophi2))) *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
generalize (age_level _ _ H0); intro.
(* Goal: @ex A (fun ophi2 : A => and (@age A AG phi2 ophi2) (@eq nat (@level A AG phi) (@level A AG ophi2))) *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
rewrite H in H2; apply levelS_age1 in H2. destruct H2 as [y ?].
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
exists y; split; auto.
(* Goal: @eq nat (@level A AG phi) (@level A AG y) *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
apply age_level in H0; apply age_level in H2; omega.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
destruct H2 as [ophi2 [? ?]].
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
specialize (IHn _ _ _ H3 H1).
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
destruct IHn as [phi2' [? ?]].
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2'))) *)
exists phi2'.
(* Goal: and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@eq nat (@level A AG phi1') (@level A AG phi2')) *)
split; trivial.
(* Goal: @eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2') *)
unfold ageN.
(* Goal: iff (@relation_power A (S n) (@age A agA) x y) (@eq (option A) (@partial_fun_power A (S n) (@age1 A agA) x) (@Some A y)) *)
simpl.
(* Goal: @eq (option A) match @age1 A AG phi2 with | Some w' => @composeOptN A (@age1 A AG) n w' | None => @None A end (@Some A phi2') *)
rewrite H2.
(* Goal: @eq (option A) (@composeOptN A (@age1 A AG) n ophi2) (@Some A phi2') *)
trivial.
Qed.

Lemma age1_join_eq {A}  {JA: Join A}{PA: Perm_alg A}{agA: ageable A}{AgeA: Age_alg A} : forall phi1 phi2 phi3,
        join phi1 phi2 phi3 ->
        forall phi1', age1 phi1 = Some phi1' ->
        forall phi2', age1 phi2 = Some phi2' ->
        forall phi3', age1 phi3 = Some phi3' ->
        join phi1' phi2' phi3'.
Proof.
(* Goal: forall (phi1 phi2 phi3 : A) (_ : @join A JA phi1 phi2 phi3) (phi1' : A) (_ : @eq (option A) (@age1 A agA phi1) (@Some A phi1')) (phi2' : A) (_ : @eq (option A) (@age1 A agA phi2) (@Some A phi2')) (phi3' : A) (_ : @eq (option A) (@age1 A agA phi3) (@Some A phi3')), @join A JA phi1' phi2' phi3' *)
intros until phi3.
(* Goal: forall (_ : @join A JA phi1 phi2 phi3) (phi1' : A) (_ : @eq (option A) (@age1 A agA phi1) (@Some A phi1')) (phi2' : A) (_ : @eq (option A) (@age1 A agA phi2) (@Some A phi2')) (phi3' : A) (_ : @eq (option A) (@age1 A agA phi3) (@Some A phi3')), @join A JA phi1' phi2' phi3' *)
intros H phi1' H0 phi2' H1 phi3' H2.
(* Goal: @join A JA phi1' phi2' phi3' *)
destruct (age1_join _ H H0) as [phi4 [x' [? [? ?]]]].
(* Goal: @age A agA (@core A JA SA x) (@core A JA SA y) *)
unfold age in *.
(* Goal: @join A JA phi1' phi2' phi3' *)
rewrite H4 in H1.
(* Goal: @ex A (fun y' : A => @relation_power A n (@age A agA) y y') *)
inversion H1.
(* Goal: @join A JA phi1' phi2' phi3' *)
rewrite <- H7.
(* Goal: @join A JA phi1' phi4 phi3' *)
rewrite H5 in H2.
(* Goal: @join A JA phi1' phi4 phi3' *)
inversion H2.
(* Goal: @join A JA phi1' phi4 phi3' *)
rewrite <- H8.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
auto.
Qed.

Lemma strong_nat_ind (P : nat -> Prop) (IH : forall n, (forall i, lt i n -> P i) -> P n) n : P n.
Proof.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
  apply IH; induction n; intros i li; inversion li; eauto.
Qed.

Lemma age_core {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall x y : A, age x y -> age (core x) (core y).
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
 intros. unfold age in *.
(* Goal: @eq (option A) (@age1 A agA (@core A JA SA x)) (@Some A (@core A JA SA y)) *)
 pose proof (core_unit x).
(* Goal: @eq (option A) (@age1 A agA (@core A JA SA x)) (@Some A (@core A JA SA y)) *)
 unfold unit_for in H0.
(* Goal: @eq (option A) (@age1 A agA (@core A JA SA x)) (@Some A (@core A JA SA y)) *)
 destruct (age1_join2 _ H0 H) as [a [b [? [? ?]]]].
(* Goal: @eq (option A) (@age1 A agA (@core A JA SA x)) (@Some A (@core A JA SA y)) *)
 unfold age in H3. rewrite H3 in H; inv H.
(* Goal: @eq (option A) (@age1 A agA (@core A JA SA x)) (@Some A (@core A JA SA y)) *)
 pose proof (core_unit y).
(* Goal: @eq (option A) (@age1 A agA (@core A JA SA x)) (@Some A (@core A JA SA y)) *)
 assert (a = core y); [|subst; auto].
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
 eapply same_identity; eauto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
 - eapply age_identity; eauto.
(* Goal: @identity A JA (@core A JA SA y) *)
   apply core_identity.
 - apply core_identity.
Qed.

Lemma necR_core {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall x y : A, necR x y -> necR (core x) (core y).
Proof.
(* Goal: forall (x y : A) (_ : @necR A agA x y), @necR A agA (@core A JA SA x) (@core A JA SA y) *)
 induction 1.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
 constructor 1; apply age_core; auto.
(* Goal: @necR A agA (@core A JA SA x) (@core A JA SA x) *)
(* Goal: @necR A agA (@core A JA SA x) (@core A JA SA z) *)
 constructor 2.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
 constructor 3 with (core y); auto.
Qed.

Definition relation_mul {A: Type} (R0 R1: relation A) (x y: A) := exists z, R0 x z /\ R1 z y.

Fixpoint relation_power {A: Type} (n: nat) (R: relation A) :=
  match n with
  | O => eq
  | S n0 => relation_mul R (relation_power n0 R)
  end.

Fixpoint partial_fun_power {A: Type} (n: nat) (f: A -> option A) (x: A) :=
  match n with
  | O => Some x
  | S n0 => match f x with
            | Some fx => partial_fun_power n0 f fx
            | None => None
            end
  end.

Lemma laterR_power_age: forall {A:Type} {agA:ageable A} (x y: A),
  laterR x y <-> (exists n, relation_power (S n) age x y).
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: iff (@laterR A agA x y) (@ex nat (fun n : nat => @relation_power A (S n) (@age A agA) x y)) *)
  remember (level x) eqn:?H.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  revert x y H; induction n; intros.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  + split; intros.
    - apply laterR_level in H0.
(* Goal: @laterR A agA y' y' *)
      omega.
    - destruct H0 as [n ?H].
(* Goal: @laterR A agA x y *)
      destruct H0 as [z [? ?]].
(* Goal: @laterR A agA y' y' *)
      apply age_level in H0; omega.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  + split; intros.
    - destruct (age1 x) as [a' |] eqn:?H; [| apply age1_level0 in H1; omega].
(* Goal: @ex nat (fun n : nat => @relation_power A (S n) (@age A agA) x y) *)
      assert (age x a') by auto; clear H1.
(* Goal: @ex nat (fun n : nat => @relation_power A (S n) (@age A agA) x y) *)
      pose proof age_later_nec _ _ _ H2 H0.
(* Goal: @ex nat (fun n : nat => @relation_power A (S n) (@age A agA) x y) *)
      destruct (nec_refl_or_later _ _ H1).
      * exists 0.
(* Goal: iff (@relation_power A (S n) (@age A agA) x y) (@eq (option A) (@partial_fun_power A (S n) (@age1 A agA) x) (@Some A y)) *)
        simpl.
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
        exists y.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
        subst; auto.
(* Goal: iff (@relation_power A (S n) (@age A agA) x y) (@eq (option A) (@partial_fun_power A (S n) (@age1 A agA) x) (@Some A y)) *)
      * simpl.
(* Goal: @ex nat (fun n : nat => @relation_mul A (@age A agA) (@relation_power A n (@age A agA)) x y) *)
        pose proof age_level _ _ H2.
        rewrite <- H in H4; inversion H4; clear H4.
(* Goal: @ex nat (fun n : nat => @relation_mul A (@age A agA) (@relation_power A n (@age A agA)) x y) *)
        destruct (IHn a' y H6) as [? _].
(* Goal: @ex nat (fun n : nat => @relation_mul A (@age A agA) (@relation_power A n (@age A agA)) x y) *)
        destruct (H4 H3) as [n0 ?H].
(* Goal: @ex nat (fun n : nat => @relation_mul A (@age A agA) (@relation_power A n (@age A agA)) x y) *)
        exists (S n0).
(* Goal: iff (@relation_power A (S n) (@age A agA) x y) (@eq (option A) (@partial_fun_power A (S n) (@age1 A agA) x) (@Some A y)) *)
        simpl.
(* Goal: @relation_mul A (@age A agA) (@relation_mul A (@age A agA) (@relation_power A n0 (@age A agA))) x y *)
        exists a'.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
        auto.
    - destruct H0 as [n0 [z [?H ?H]]].
(* Goal: @laterR A agA x y *)
      pose proof age_level _ _ H0.
      rewrite <- H in H2; inversion H2; clear H2.
(* Goal: @laterR A agA x y *)
      destruct (IHn z y H4) as [_ ?H].
(* Goal: @laterR A agA x y *)
      destruct n0.
(* Goal: @laterR A agA y y' *)
      * simpl in H1; subst.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
        apply t_step; auto.
      * spec H2; [exists n0; auto |].
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
        eapply t_trans; eauto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
        apply t_step; auto.
Qed.

Lemma necR_power_age: forall {A:Type} {agA:ageable A} (x y: A),
  necR x y <-> (exists n, relation_power n age x y).
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  split; intros.
  + destruct (nec_refl_or_later _ _ H).
(* Goal: @laterR A agA y y' *)
    - subst.
(* Goal: @ex nat (fun n : nat => @relation_power A n (@age A agA) y y) *)
      exists 0.
(* Goal: iff (@relation_power A (S n) (@age A agA) x y) (@eq (option A) (@partial_fun_power A (S n) (@age1 A agA) x) (@Some A y)) *)
      simpl.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
      auto.
    - destruct (laterR_power_age x y) as [? _].
(* Goal: @ex nat (fun n : nat => @relation_power A n (@age A agA) x y) *)
      destruct (H1 H0) as [n0 ?H].
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
      exists (S n0); auto.
  + destruct H as [n ?H].
(* Goal: @necR A agA x y *)
    destruct n.
(* Goal: @laterR A agA y y' *)
    - simpl in H; subst.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
      auto.
    - destruct (laterR_power_age x y) as [_ ?].
(* Goal: @necR A agA x y *)
      spec H0; [exists n; auto |].
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
      apply laterR_necR; auto.
Qed.

Lemma power_age_age1: forall {A:Type} {agA:ageable A} n x y,
  relation_power n age x y <-> partial_fun_power n age1 x = Some y.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  revert x; induction n; intros.
(* Goal: iff (@relation_power A (S n) (@age A agA) x y) (@eq (option A) (@partial_fun_power A (S n) (@age1 A agA) x) (@Some A y)) *)
  + simpl.
(* Goal: iff (@eq A x y) (@eq (option A) (@Some A x) (@Some A y)) *)
    split; intros; [subst| inversion H]; reflexivity.
(* Goal: iff (@relation_power A (S n) (@age A agA) x y) (@eq (option A) (@partial_fun_power A (S n) (@age1 A agA) x) (@Some A y)) *)
  + simpl.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
    split; intros.
    - destruct H as [z [?H ?H]].
(* Goal: @eq nat (@level A agA x') (@level A agA x) *)
      rewrite H.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
      apply IHn; auto.
    - destruct (age1 x) as [z |] eqn:?H; [| inversion H].
(* Goal: @relation_mul A (@age A agA) (@relation_power A n (@age A agA)) x y *)
      exists z.
(* Goal: and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y')) *)
      split; [auto |].
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
      apply IHn; auto.
Qed.

Lemma power_age1_level_small: forall {A:Type} {agA:ageable A} n x,
  partial_fun_power n age1 x = None <-> level x < n.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  revert x; induction n; intros.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  + simpl; split; intros.
    - inversion H.
    - omega.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  + simpl; split; intros.
    - destruct (age1 x) eqn:?H.
      * apply age_level in H0.
(* Goal: lt (@level A agA x) (S n) *)
        apply IHn in H.
(* Goal: @laterR A agA y' y' *)
        omega.
      * apply age1_level0 in H0.
(* Goal: @laterR A agA y' y' *)
        omega.
    - destruct (age1 x) eqn:?H.
      * apply IHn.
(* Goal: lt (@level A agA a) n *)
        apply age_level in H0.
(* Goal: @laterR A agA y' y' *)
        omega.
      * reflexivity.
Qed.

Lemma power_age_core: forall {A:Type} {agA:ageable A} {JA: Join A} {PA: Perm_alg A} {SaA: Sep_alg A} {XA: Age_alg A} (x y: A) n,
  relation_power n age x y -> relation_power n age (core x) (core y).
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  revert x y H; induction n; intros.
  + simpl in H |- *.
(* Goal: @eq nat (@level A agA x') (@level A agA x') *)
    subst; reflexivity.
  + simpl in H |- *.
(* Goal: @relation_mul A (@age A agA) (@relation_power A n (@age A agA)) (@core A JA SaA x) (@core A JA SaA y) *)
    destruct H as [z [?H ?H]].
(* Goal: @relation_mul A (@age A agA) (@relation_power A n (@age A agA)) (@core A JA SaA x) (@core A JA SaA y) *)
    exists (core z).
(* Goal: and (@necR A agA y y) (@eq nat (@level A agA x') (@level A agA y)) *)
    split.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    - apply age_core; auto.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    - apply IHn; auto.
Qed.

Lemma power_age_core_eq: forall {A:Type} {agA:ageable A} {JA: Join A} {PA: Perm_alg A} {SaA: Sep_alg A} {XA: Age_alg A} (x x' y y': A) n,
  relation_power n age x x' -> relation_power n age y y' -> core x = core y -> core x' = core y'.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  revert x y H H0 H1; induction n; intros.
  + simpl in H, H0 |- *.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    subst; auto.
  + simpl in H, H0 |- *.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    destruct H as [x'' [?H ?H]].
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    destruct H0 as [y'' [?H ?H]].
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    pose proof age_core_eq _ _ _ _ H H0 H1.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    specialize (IHn x'' y'' H2 H3 H4).
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    auto.
Qed.

Lemma levelS_age {A: Type} {agA: ageable A} : forall (x:A) n,
  S n = level x ->
  exists y, age x y /\ n = level y.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: @ex A (fun y : A => and (@age A agA x y) (@eq nat n (@level A agA y))) *)
  apply eq_sym in H.
(* Goal: @ex A (fun y : A => and (@age A agA x y) (@eq nat n (@level A agA y))) *)
  remember H as H0; clear HeqH0.
(* Goal: @ex A (fun y : A => and (@age A agA x y) (@eq nat n (@level A agA y))) *)
  apply levelS_age1 in H0.
(* Goal: @ex A (fun y : A => and (@age A agA x y) (@eq nat n (@level A agA y))) *)
  destruct H0 as [y ?].
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  exists y.
(* Goal: and (@age A agA x y) (@eq nat n (@level A agA y)) *)
  assert (age x y).
(* Goal: @age A agA x y *)
(* Goal: and (@age A agA x y) (@eq nat n (@level A agA y)) *)
  unfold age.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
(* Goal: @ex A (fun y' : A => and (@laterR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  exact H0.
(* Goal: and (@necR A agA y y) (@eq nat (@level A agA x') (@level A agA y)) *)
  split.
(* Goal: @laterR A agA y y' *)
  exact H1.
(* Goal: @eq nat n (@level A agA y) *)
  apply age_level in H1.
(* Goal: @eq nat n (@level A agA y) *)
  rewrite H in H1.
(* Goal: @ex A (fun y' : A => @relation_power A n (@age A agA) y y') *)
  inversion H1.
(* Goal: @eq nat (@level A agA x') (@level A agA x') *)
  reflexivity.
Qed.

Lemma clos_refl_trans_addone: forall (A : Type) (R : relation A) (x y z: A), R x y -> clos_refl_trans A R y z -> clos_refl_trans A R x z.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: clos_refl_trans A R x z *)
  apply (rt_step A R x y) in H.
(* Goal: clos_refl_trans A R x z *)
  apply rt_trans with y.
(* Goal: @necR A agA x x' *)
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
(* Goal: @ex A (fun y' : A => and (@laterR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  exact H.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
(* Goal: @ex A (fun y' : A => and (@laterR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  exact H0.
Qed.

Lemma necR_same_level: forall {A:Type} {agA:ageable A} (x y x': A), necR x x' -> level x = level y -> exists y', (necR y y' /\ level x' = level y').
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (x y x' : A) (_ : @necR A agA x x') (_ : @eq nat (@level A agA x) (@level A agA y)), @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  intros A agA x y.
(* Goal: forall (x' : A) (_ : @necR A agA x x') (_ : @eq nat (@level A agA x) (@level A agA y)), @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  remember (level x) as n.
(* Goal: forall (x' : A) (_ : @necR A agA x x') (_ : @eq nat n (@level A agA y)), @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  generalize Heqn; clear Heqn.
(* Goal: forall (_ : @eq nat n (@level A agA x)) (x' : A) (_ : @necR A agA x x') (_ : @eq nat n (@level A agA y)), @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  generalize x y; clear x y.
(* Goal: forall (x y : A) (_ : @eq nat n (@level A agA x)) (x' : A) (_ : @necR A agA x x') (_ : @eq nat n (@level A agA y)), @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  induction n.
  (* basic step *)
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  + intros.
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
    apply necR_level in H.
    rewrite <- Heqn in H.
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
    destruct (level x') eqn:HH; [|omega].
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
    exists y.
(* Goal: and (@necR A agA y y) (@eq nat (@level A agA x') (@level A agA y)) *)
    split.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
       unfold necR; auto.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
(* Goal: @ex A (fun y' : A => and (@laterR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
       exact H0.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  + intros.
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
    apply nec_refl_or_later in H.
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
    destruct H.
    - exists y.
(* Goal: and (@necR A agA y y) (@eq nat (@level A agA x') (@level A agA y)) *)
      split.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
         unfold necR; auto.
         rewrite <- H0. rewrite -> Heqn. rewrite H. reflexivity.
    - apply levelS_age in H0; destruct H0 as [y'' [? ?]].
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
      apply levelS_age in Heqn; destruct Heqn as [x'' [? ?]].
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
      remember (IHn x'' y'' H3 x') as HH; clear HeqHH.
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
      assert(necR x'' x').
(* Goal: @necR A agA x'' x' *)
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
        apply (age_later_nec x); [exact H2 | exact H].
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
      apply HH in H4; clear HH; [|exact H1].
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
      destruct H4 as [y' [? ?]].
(* Goal: @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
      exists y'.
(* Goal: and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y')) *)
      split; [| exact H5].
(* Goal: @necR A agA y y' *)
      unfold necR.
(* Goal: clos_refl_trans A (@age A agA) y y' *)
      apply clos_refl_trans_addone with y''; [exact H0| exact H4].
Qed.

Lemma laterR_same_level: forall {A:Type} {agA:ageable A} (x y x': A), laterR x x' -> level x = level y -> exists y', (laterR y y' /\ level x' = level y').
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: @necR A agA x x' *)
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
(* Goal: @ex A (fun y' : A => and (@laterR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  assert (HH: laterR x x'). exact H.
(* Goal: @ex A (fun y' : A => and (@laterR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  apply laterR_necR in H.
(* Goal: @ex A (fun y' : A => and (@laterR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  assert (exists y' : A, necR y y' /\ level x' = level y').
(* Goal: @ex A (fun y' : A => and (@necR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
(* Goal: @ex A (fun y' : A => and (@laterR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
     apply (necR_same_level x y).
(* Goal: @necR A agA x x' *)
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
(* Goal: @ex A (fun y' : A => and (@laterR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
     exact H.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
(* Goal: @ex A (fun y' : A => and (@laterR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
     exact H0.
(* Goal: @ex A (fun y' : A => and (@laterR A agA y y') (@eq nat (@level A agA x') (@level A agA y'))) *)
  destruct H1 as [y' [? ?]].
(* Goal: @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  exists y'.
(* Goal: and (@laterR A agA y y') (@eq nat (@level A agA x') (@level A agA y')) *)
  split; [|exact H2].
(* Goal: @laterR A agA y y' *)
  apply nec_refl_or_later in H1.
(* Goal: @laterR A agA y y' *)
  destruct H1.
  + apply laterR_level in HH.
(* Goal: @laterR A agA y y' *)
    subst.
    rewrite <- H0 in H2.
(* Goal: @laterR A agA y' y' *)
    omega.
  + exact H1.
Qed.

Lemma power_age_parallel: forall {A:Type} {agA:ageable A} (x x' y: A) n,
  level x = level y ->
  relation_power n age x x' ->
  exists y', relation_power n age y y'.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: @ex A (fun y' : A => @relation_power A n (@age A agA) y y') *)
  destruct (partial_fun_power n age1 y) eqn:?H.
(* Goal: @ex A (fun y' : A => @relation_power A n (@age A agA) y y') *)
  + exists a.
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
    apply power_age_age1; auto.
  + apply power_age_age1 in H0.
(* Goal: @ex A (fun y' : A => @relation_power A n (@age A agA) y y') *)
    apply power_age1_level_small in H1.
    rewrite <- H in H1.
(* Goal: @ex A (fun y' : A => @relation_power A n (@age A agA) y y') *)
    apply power_age1_level_small in H1.
(* Goal: @ex A (fun y' : A => @relation_power A n (@age A agA) y y') *)
    rewrite H0 in H1.
(* Goal: @ex A (fun y' : A => @relation_power A n (@age A agA) y y') *)
    inversion H1.
Qed.

Lemma power_age_parallel': forall {A:Type} {agA:ageable A} {JA: Join A} {PA: Perm_alg A} {SaA: Sep_alg A} {XA: Age_alg A} (x x' y: A) n,
  core x = core y ->
  relation_power n age x x' ->
  exists y', relation_power n age y y' /\ core x' = core y'.
Proof.
(* Goal: forall (A : Type) (agA : ageable A) (JA : Join A) (_ : @Perm_alg A JA) (SaA : @Sep_alg A JA) (_ : @Age_alg A JA agA) (x x' y : A) (n : nat) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @relation_power A n (@age A agA) x x'), @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  intros.
(* Goal: @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  assert (level x = level y).
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
(* Goal: @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  1:{
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
    pose proof level_core y.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
    pose proof level_core x.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
    rewrite H in H2.
(* Goal: @eq nat (@level A agA x) (@level A agA y) *)
    congruence.
  }
(* Goal: @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  destruct (power_age_parallel x x' y n H1 H0) as [y' ?H].
(* Goal: @ex A (fun y' : A => and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y'))) *)
  exists y'.
(* Goal: and (@relation_power A n (@age A agA) y y') (@eq A (@core A JA SaA x') (@core A JA SaA y')) *)
  split; [auto |].
(* Goal: @eq A (@core A JA SaA x') (@core A JA SaA y') *)
  eapply power_age_core_eq; eauto.
Qed.

