Require Import VST.msl.msl_standard.
Require Import VST.msl.ghost.
Require Import VST.msl.Coqlib2.
Require Import VST.veric.shares.

Module Type ADR_VAL.
Parameter address : Type.
Parameter some_address:address.

(* Validity of traces.  The "valid" predicate ensures that related addresses don't get
    split apart from each other.  *)
Parameter kind: Type.
End ADR_VAL.

Inductive TypeTree: Type :=
  | ConstType: Type -> TypeTree
  | Mpred: TypeTree
  | DependentType: nat -> TypeTree
  | ProdType: TypeTree -> TypeTree -> TypeTree
  | ArrowType: TypeTree -> TypeTree -> TypeTree
  | PiType: forall (I : Type), (I -> TypeTree) -> TypeTree
  | ListType: TypeTree -> TypeTree.

Definition dependent_type_functor_rec (ts: list Type): TypeTree -> functor :=
  fix dtfr (T: TypeTree): functor :=
  match T with
  | ConstType A => fconst A
  | Mpred => fidentity
  | DependentType n => fconst (nth n ts unit)
  | ProdType T1 T2 => fpair (dtfr T1) (dtfr T2)
  | ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2)
  | PiType _ f => fpi (fun i => dtfr (f i))
  | ListType T => flist (dtfr T)
  end.
Opaque dependent_type_functor_rec.

Definition dependent_type_function_rec (ts: list Type) (mpred': Type): TypeTree -> Type :=
  fix dtfr (T: TypeTree): Type :=
  match T with
  | ConstType A => A
  | Mpred => mpred'
  | DependentType n => nth n ts unit
  | ProdType T1 T2 => (dtfr T1 * dtfr T2)%type
  | ArrowType T1 T2 => dtfr T1 -> dtfr T2
  | PiType A f => forall a, dtfr (f a)
  | ListType T => list (dtfr T)
  end.

Definition fpreds: functor :=
  fsig (fun T: TypeTree =>
    fpi (fun ts: list Type => dependent_type_functor_rec ts T)).

Lemma realize_eq: forall {A} (a b: A) P, (exists H: a = b, P H) -> {H: a = b & P H}.
Proof.
(* Goal: forall (A : Type) (a b : A) (P : forall _ : @eq A a b, Prop) (_ : @ex (@eq A a b) (fun H : @eq A a b => P H)), @sigT (@eq A a b) (fun H : @eq A a b => P H) *)
  intros ???? []; subst; exists eq_refl; auto.
Qed.

Lemma lower_join_inv : forall {A} {J: Join A} a b c, lower_join J a b c <->
  match a, b, c with
  | Some a, Some b, Some c => join a b c
  | Some a, None, Some c | None, Some a, Some c => a = c
  | None, None, None => True
  | _, _, _ => False
  end.
Proof.
(* Goal: and (lt (@level rmap ag_rmap a') n) (@app_pred rmap ag_rmap p a') *)
  split.
  - inversion 1; subst; auto; destruct c; auto.
  - destruct a, b, c; intros; subst; try contradiction; try constructor; auto.
Qed.

Module Type STRAT_MODEL.
  Declare Module AV : ADR_VAL.
  Import AV.

  Inductive res (PRED : Type) : Type :=
    | NO':  forall sh: Share.t, ~(readable_share sh) -> res PRED
    | YES': forall sh: Share.t, readable_share sh -> kind -> fpreds PRED -> res PRED
    | PURE': kind -> fpreds PRED -> res PRED.

  Definition res_fmap (A B:Type) (f:A->B) (g:B->A)(x:res A) : res B :=
    match x with
      | NO' rsh nsh => NO' B rsh nsh
      | YES' sh rsh k pds => YES' B sh rsh k (fmap fpreds f g pds)
      | PURE' k pds => PURE' B k (fmap fpreds f g pds)
    end.
  Axiom ff_res : functorFacts res res_fmap.
  Definition f_res : functor := Functor ff_res.

  Inductive res_join (PRED : Type) : f_res PRED -> f_res PRED -> f_res PRED -> Prop :=
    | res_join_NO1 : forall sh1 nsh1 sh2 nsh2 sh3 nsh3,
                               join sh1 sh2 sh3 ->
                               res_join PRED (NO' PRED sh1 nsh1) (NO' PRED sh2 nsh2) 
                                     (NO' PRED sh3 nsh3)
    | res_join_NO2 : forall sh1 nsh1 sh2 rsh2 sh3 rsh3 k p,
                               join sh1 sh2 sh3 ->
                               res_join PRED (NO' PRED sh1 nsh1) (YES' PRED sh2 rsh2 k p) 
                                   (YES' PRED sh3 rsh3 k p)
    | res_join_NO3 : forall sh1 rsh1 sh2 nsh2 sh3 rsh3 k p,
                               join sh1 sh2 sh3 ->
                               res_join PRED (YES' PRED sh1 rsh1 k p) (NO' PRED sh2 nsh2) 
                                   (YES' PRED sh3 rsh3 k p)
    | res_join_YES : forall sh1 rsh1 sh2 rsh2 sh3 rsh3 k p,
                              join sh1 sh2 sh3 ->
              res_join PRED (YES' PRED sh1 rsh1 k p) (YES' PRED sh2 rsh2 k p) (YES' PRED sh3 rsh3 k p)
    | res_join_PURE : forall k p, res_join PRED (PURE' PRED k p) (PURE' PRED k p) (PURE' PRED k p).
  Axiom pa_rj : forall PRED, @Perm_alg _ (res_join PRED).
  Instance sa_rj : forall PRED, @Sep_alg _ (res_join PRED).
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
  Proof. intros.
            apply mkSep 
             with (fun x => match x 
                             with NO' _ _ => NO' _ Share.bot bot_unreadable
                               | YES' _ _ _ _ => NO' _ Share.bot bot_unreadable
                               | PURE' k pds => PURE' _ k pds end).
(* Goal: forall x : rmap', @eq rmap' (pre_rmap2rmap' (rmap'2pre_rmap x)) x *)
            intro. destruct t; constructor; try apply join_unit1; auto.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
            intros. inversion H; auto.
  Defined.

  Axiom paf_res : @pafunctor f_res res_join.

  Definition res_option (PRED : Type) (r: res PRED) : option (rshare * kind):=
    match r with
      | NO' _ _ => None
      | YES' sh rsh k _ => Some (readable_part rsh,k)
      | PURE' _ _ => None (* PUREs cannot be split in any interesting way, which is what valid is about. *)
    end.

  Definition ghost (PRED : Type) : Type :=
    list (option ({g: Ghost & {a: @G g | ghost.valid a}} * fpreds PRED)%type).

  Definition ghost_fmap (A B:Type) (f:A->B) (g:B->A)(x:ghost A) : ghost B :=
    fmap (flist (foption (fpair (fconst _) fpreds))) f g x.

  Axiom ff_ghost : functorFacts ghost ghost_fmap.
  Definition f_ghost : functor := Functor ff_ghost.

  Instance preds_join PRED : Join _ := Join_equiv (fpreds PRED).

(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join b c f) (@join ghost ghost_join (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) f e)) *)
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join b c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
  Inductive ghost_elem_join : Join {g: Ghost & {a: @G g | ghost.valid a}} :=
  | elem_join_I g a b c va vb vc: join a b c ->
    ghost_elem_join (existT _ g (exist _ a va)) (existT _ g (exist _ b vb))
                    (existT _ g (exist _ c vc)).
  Existing Instance ghost_elem_join.

  Inductive ghost_join PRED : Join (ghost PRED) :=
  | ghost_join_nil_l m: ghost_join PRED nil m m
  | ghost_join_nil_r m: ghost_join PRED m nil m
  | ghost_join_cons a1 a2 m1 m2 a3 m3: join a1 a2 a3 -> ghost_join PRED m1 m2 m3 ->
      ghost_join PRED (a1 :: m1) (a2 :: m2) (a3 :: m3).
  Existing Instance ghost_join.

  Axiom pa_gj : forall PRED, @Perm_alg _ (ghost_join PRED).

  Instance sa_gj : forall PRED, @Sep_alg _ (ghost_join PRED).
  Proof.
(* Goal: @Sep_alg ghost ghost_join *)
    intros; exists (fun _ => nil); auto; constructor.
  Defined.
  Axiom paf_ghost : @pafunctor f_ghost ghost_join.

  Definition f_pre_rmap : functor :=
    fpair (ffunc (fconst address) f_res) f_ghost.

  Instance Join_pre_rmap (A: Type) : Join (f_pre_rmap A) :=
            Join_prod _ (Join_fun address (res A) (res_join A)) _ (ghost_join A).

  Declare Instance Perm_pre_rmap: forall (A: Type), Perm_alg (f_pre_rmap A).
  Declare Instance Sep_pre_rmap: forall (A: Type), Sep_alg (f_pre_rmap A).
  Parameter paf_pre_rmap : @pafunctor f_pre_rmap Join_pre_rmap.

  Existing Instance ghost_join.
  Instance Join_res A : Join (f_res A) := res_join A.

Axiom pre_rmap_core:
forall (A : Type) (m : f_pre_rmap A),
  @core (f_pre_rmap A) (Join_pre_rmap A) (Sep_pre_rmap A) m =
 (@core ((fpair (ffunc (fconst address) f_res) f_ghost) A)
           (Join_prod ((ffunc (fconst address) f_res) A)
              (Join_pi ((fconst address) A)
                 (fun _ : (fconst address) A => f_res A)
                 (fun _ : (fconst address) A => Join_res A))
              (f_ghost A) (ghost_join A))
           (@Sep_prod ((ffunc (fconst address) f_res) A)
              (Join_pi ((fconst address) A)
                 (fun _ : (fconst address) A => f_res A)
                 (fun _ : (fconst address) A => Join_res A))
              (f_ghost A) (ghost_join A)
              (Sep_pi ((fconst address) A)
                 (fun _ : (fconst address) A => f_res A)
                 (fun _ : (fconst address) A => Join_res A)
                 (fun _ : (fconst address) A => sa_rj A)) 
              (sa_gj A)) m).

End STRAT_MODEL.

Module StratModel (AV' : ADR_VAL) : STRAT_MODEL with Module AV:=AV'.
  Module AV := AV'.
  Import AV.

  Definition preds: functor :=
    fsig (fun T: TypeTree =>
      fpi (fun ts: list Type => dependent_type_functor_rec ts T)).

  Inductive res (PRED : Type) : Type :=
    | NO':  forall sh: Share.t, ~(readable_share sh) -> res PRED
    | YES': forall sh: Share.t, readable_share sh -> kind -> preds PRED -> res PRED
    | PURE': kind -> preds PRED -> res PRED.

  Definition res_fmap (A B:Type) (f:A->B) (g:B->A)(x:res A) : res B :=
    match x with
      | NO' rsh nsh => NO' B rsh nsh
      | YES' sh rsh k pds => YES' B sh rsh k (fmap preds f g pds)
      | PURE' k pds => PURE' B k (fmap preds f g pds)
    end.

  Lemma ff_res : functorFacts res res_fmap.
  Proof with auto.
    constructor; intros; extensionality rs; icase rs; unfold res_fmap.
    rewrite fmap_id... rewrite fmap_id...
    rewrite <- fmap_comp... rewrite <- fmap_comp...
  Qed.

  Definition f_res : functor := Functor ff_res.

  Inductive res_join (PRED : Type) : f_res PRED -> f_res PRED -> f_res PRED -> Prop :=
    | res_join_NO1 : forall sh1 nsh1 sh2 nsh2 sh3 nsh3,
                               join sh1 sh2 sh3 ->
                               res_join PRED (NO' PRED sh1 nsh1) (NO' PRED sh2 nsh2) 
                                     (NO' PRED sh3 nsh3)
    | res_join_NO2 : forall sh1 nsh1 sh2 rsh2 sh3 rsh3 k p,
                               join sh1 sh2 sh3 ->
                               res_join PRED (NO' PRED sh1 nsh1) (YES' PRED sh2 rsh2 k p) 
                                   (YES' PRED sh3 rsh3 k p)
    | res_join_NO3 : forall sh1 rsh1 sh2 nsh2 sh3 rsh3 k p,
                               join sh1 sh2 sh3 ->
                               res_join PRED (YES' PRED sh1 rsh1 k p) (NO' PRED sh2 nsh2) 
                                   (YES' PRED sh3 rsh3 k p)
    | res_join_YES : forall sh1 rsh1 sh2 rsh2 sh3 rsh3 k p,
                              join sh1 sh2 sh3 ->
              res_join PRED (YES' PRED sh1 rsh1 k p) (YES' PRED sh2 rsh2 k p) (YES' PRED sh3 rsh3 k p)
    | res_join_PURE : forall k p, res_join PRED (PURE' PRED k p) (PURE' PRED k p) (PURE' PRED k p).

  Instance Join_res (PRED: Type) : Join (res PRED) := res_join PRED.

  Instance pa_rj : forall PRED, @Perm_alg _ (res_join PRED).
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
  Proof. intros. constructor.
*      (* saf_eq *)
      intros x y z z' H1 H2; inv H1; inv H2;
      repeat match goal with H: join ?A ?B _, H': join ?A ?B ?C |- _ => pose proof (join_eq H H'); subst C end;
(* Goal: @eq nat n n *)
      repeat proof_irr; auto.
*     (* saf_assoc *)
(* Goal: forall (a b c d e : resource) (_ : @join resource Join_resource a b d) (_ : @join resource Join_resource d c e), @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      intros a b c d e H1 H2.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct d as [rd | rd sd kd pd | kd pd].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct a as [ra | | ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource (NO ra n0) f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct b as [rb| | ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (NO rb n1) c f) (@join resource Join_resource (NO ra n0) f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (join ra rb rd) by (inv H1; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct c as [rc | rc sc kc pc | kc pc]; try solve [elimtype False; inv H2].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct e as [re | re se ke pe | ke pe]; try solve [elimtype False; inv H2].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (NO rb n1) (YES rc sc kc pc) f) (@join resource Join_resource (NO ra n0) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (join rd rc re) by (inv H2; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: @sigT (_functor f_res PRED) (fun f : _functor f_res PRED => and (@join (_functor f_res PRED) (res_join PRED) (NO' PRED rb n1) (NO' PRED rc n2) f) (@join (_functor f_res PRED) (res_join PRED) (NO' PRED ra n0) f (NO' PRED re n3))) *)
(* Goal: @sigT (_functor f_res PRED) (fun f : _functor f_res PRED => and (@join (_functor f_res PRED) (res_join PRED) (NO' PRED rb n1) (YES' PRED rc sc kc pc) f) (@join (_functor f_res PRED) (res_join PRED) (NO' PRED ra n0) f e)) *)
(* Goal: @sigT (_functor f_res PRED) (fun f : _functor f_res PRED => and (@join (_functor f_res PRED) (res_join PRED) b c f) (@join (_functor f_res PRED) (res_join PRED) a f e)) *)
(* Goal: @sigT (_functor f_res PRED) (fun f : _functor f_res PRED => and (@join (_functor f_res PRED) (res_join PRED) b c f) (@join (_functor f_res PRED) (res_join PRED) a f e)) *)
      exists (NO' _ rf (join_unreadable_shares H3 n1 n2)); split; constructor; auto.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct e as [re | re se ke pe | ke pe]; try solve [elimtype False; inv H2].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (NO rb n1) (YES rc sc kc pc) f) (@join resource Join_resource (NO ra n0) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (join rd rc re) by (inv H2; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: @sigT (_functor f_res PRED) (fun f : _functor f_res PRED => and (@join (_functor f_res PRED) (res_join PRED) (NO' PRED rb n) (YES' PRED rc sc kc pc) f) (@join (_functor f_res PRED) (res_join PRED) (YES' PRED ra sa ka pa) f (YES' PRED re se ke pe))) *)
(* Goal: @sigT (_functor f_res PRED) (fun f : _functor f_res PRED => and (@join (_functor f_res PRED) (res_join PRED) (YES' PRED rb sb kb pb) (YES' PRED rc sc kc pc) f) (@join (_functor f_res PRED) (res_join PRED) a f (YES' PRED re se ke pe))) *)
(* Goal: @sigT (_functor f_res PRED) (fun f : _functor f_res PRED => and (@join (_functor f_res PRED) (res_join PRED) b c f) (@join (_functor f_res PRED) (res_join PRED) a f e)) *)
      exists (YES' _ rf (join_readable2 H3 sc) kc pc).
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc kc pc) (YES rf (@join_readable2 rb rc rf H3 sc) kc pc)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) kc pc) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      inv H2. split; constructor; auto.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct c as [rc | rc sc kc pc | kc pc]; try solve [elimtype False; inv H2].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct e as [re | re se ke pe | ke pe]; try solve [elimtype False; inv H2].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H0: join rd rc re) by (inv H2; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct a as [ra | ra sa ka pa | ka pa ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (NO rc n) f) (@join resource Join_resource (NO ra n0) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (NO rc n) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct b as [ | rb sb kb pb | ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H: join ra rb rd) by (inv H1; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      exists (YES' _ rf (join_readable1 H3 sb) kd pd).  inv H1; inv H2; split; constructor; auto.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct b as [ rb | rb sb kb pb | ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H: join ra rb rd) by (inv H1; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      exists (NO' _ rf (join_unreadable_shares H3 n0 n)).  inv H1; inv H2; split; constructor; auto.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H: join ra rb rd) by (inv H1; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      exists (YES' _ rf (join_readable1 H3 sb) kb pb).  inv H1; inv H2; split; constructor; auto.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct e as [re | re se ke pe | ke pe]; try solve [elimtype False; inv H2].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H0: join rd rc re) by (inv H2; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct b as [ rb | rb sb kb pb | ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct a as [ra | ra sa ka pa | ka pa ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H: join ra rb rd) by (inv H1; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: @sigT (_functor f_res PRED) (fun f : _functor f_res PRED => and (@join (_functor f_res PRED) (res_join PRED) (NO' PRED rb n) (YES' PRED rc sc kc pc) f) (@join (_functor f_res PRED) (res_join PRED) (YES' PRED ra sa ka pa) f (YES' PRED re se ke pe))) *)
(* Goal: @sigT (_functor f_res PRED) (fun f : _functor f_res PRED => and (@join (_functor f_res PRED) (res_join PRED) (YES' PRED rb sb kb pb) (YES' PRED rc sc kc pc) f) (@join (_functor f_res PRED) (res_join PRED) a f (YES' PRED re se ke pe))) *)
(* Goal: @sigT (_functor f_res PRED) (fun f : _functor f_res PRED => and (@join (_functor f_res PRED) (res_join PRED) b c f) (@join (_functor f_res PRED) (res_join PRED) a f e)) *)
      exists (YES' _ rf (join_readable2 H3 sc) kc pc).  inv H1; inv H2; split; constructor; auto.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct a as [ra | ra sa ka pa | ka pa ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H: join ra rb rd) by (inv H1; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: @sigT (_functor f_res PRED) (fun f : _functor f_res PRED => and (@join (_functor f_res PRED) (res_join PRED) (YES' PRED rb sb kb pb) (YES' PRED rc sc kc pc) f) (@join (_functor f_res PRED) (res_join PRED) (YES' PRED ra sa ka pa) f (YES' PRED re se ke pe))) *)
(* Goal: @sigT (_functor f_res PRED) (fun f : _functor f_res PRED => and (@join (_functor f_res PRED) (res_join PRED) b c f) (@join (_functor f_res PRED) (res_join PRED) a f e)) *)
      exists (YES' _ rf (join_readable1 H3 sb) kb pb).  inv H1; inv H2; split; try constructor; auto.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H: join ra rb rd) by (inv H1; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: @sigT (_functor f_res PRED) (fun f : _functor f_res PRED => and (@join (_functor f_res PRED) (res_join PRED) (YES' PRED rb sb kb pb) (YES' PRED rc sc kc pc) f) (@join (_functor f_res PRED) (res_join PRED) (YES' PRED ra sa ka pa) f (YES' PRED re se ke pe))) *)
(* Goal: @sigT (_functor f_res PRED) (fun f : _functor f_res PRED => and (@join (_functor f_res PRED) (res_join PRED) b c f) (@join (_functor f_res PRED) (res_join PRED) a f e)) *)
      exists (YES' _ rf (join_readable1 H3 sb) kb pb).  inv H1; inv H2; split; try constructor; auto.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
      exists (PURE' _ kd pd). inv H1; inv H2; split; constructor.

*      (* saf_com *)
(* Goal: @eq nat n n *)
      intros a b c H; inv H; econstructor;  apply join_comm; auto.

*     (* saf_positivity *)
     intros; inv H; inv H0; 
      repeat match goal with H: join ?A ?B ?C, H': join ?C ?D ?A |- _ => 
                    pose proof (join_positivity H H'); subst C 
      end; 
(* Goal: @eq nat n n *)
      repeat proof_irr; auto.
 Qed.

  Instance sa_rj : forall PRED, @Sep_alg _ (res_join PRED).
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
  Proof. intros.
            apply mkSep 
             with (fun x => match x 
                             with NO' _ _ => NO' _ Share.bot bot_unreadable
                               | YES' _ _ _ _ => NO' _ Share.bot bot_unreadable
                               | PURE' k pds => PURE' _ k pds end).
(* Goal: forall x : rmap', @eq rmap' (pre_rmap2rmap' (rmap'2pre_rmap x)) x *)
            intro. destruct t; constructor; try apply join_unit1; auto.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
            intros. inversion H; auto.
  Defined.

  Definition paf_res : @pafunctor f_res res_join.
(* Goal: forall x : rmap', @eq rmap' (pre_rmap2rmap' (rmap'2pre_rmap x)) x *)
  Proof. constructor; repeat intro.
  (* This is a little painful because of the way res_join is defined, but
      whatever... *)
(* Goal: @join (_functor f_res B) (res_join B) (@fmap f_res A B f g x) (@fmap f_res A B f g y) (@fmap f_res A B f g z) *)
(* Goal: @sigT (_functor f_res A) (fun x : _functor f_res A => @sig (_functor f_res A) (fun y0 : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g x) x') (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y))))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   inv H; simpl; constructor; trivial.
(* Goal: @sigT (_functor f_res A) (fun x : _functor f_res A => @sig (_functor f_res A) (fun y0 : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g x) x') (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y))))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   destruct z as [ rz | rz sz kz pz | kz pz ].
(* Goal: @sigT (_functor f_res A) (fun x : _functor f_res A => @sig (_functor f_res A) (fun y0 : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 (YES' A rz sz kz pz)) (and (@eq (_functor f_res B) (@fmap f_res A B f g x) x') (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y))))) *)
(* Goal: @sigT (_functor f_res A) (fun x : _functor f_res A => @sig (_functor f_res A) (fun y0 : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 (PURE' A kz pz)) (and (@eq (_functor f_res B) (@fmap f_res A B f g x) x') (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y))))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   destruct x' as [ rx' | rx' sx' kx' px' | kx' px' ]; try solve [elimtype False; inv H].
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (YES' A rx sx kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (PURE' A kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   destruct y as [ ry | ry sy ky py | ky py ]; try solve [elimtype False; inv H].
(* Goal: @sigT (_functor f_res A) (fun x : _functor f_res A => @sig (_functor f_res A) (fun y0 : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 (NO' A rz n)) (and (@eq (_functor f_res B) (@fmap f_res A B f g x) (NO' B rx' n0)) (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g (NO' A ry n1)))))) *)
(* Goal: @sigT (_functor f_res A) (fun x : _functor f_res A => @sig (_functor f_res A) (fun y0 : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 (YES' A rz sz kz pz)) (and (@eq (_functor f_res B) (@fmap f_res A B f g x) x') (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y))))) *)
(* Goal: @sigT (_functor f_res A) (fun x : _functor f_res A => @sig (_functor f_res A) (fun y0 : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 (PURE' A kz pz)) (and (@eq (_functor f_res B) (@fmap f_res A B f g x) x') (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y))))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   exists (NO' _ rx' n0); exists (NO' _ ry n1); inv H; split; constructor; tauto.
(* Goal: @sigT (_functor f_res A) (fun x : _functor f_res A => @sig (_functor f_res A) (fun y0 : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 (YES' A rz sz kz pz)) (and (@eq (_functor f_res B) (@fmap f_res A B f g x) x') (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y))))) *)
(* Goal: @sigT (_functor f_res A) (fun x : _functor f_res A => @sig (_functor f_res A) (fun y0 : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 (PURE' A kz pz)) (and (@eq (_functor f_res B) (@fmap f_res A B f g x) x') (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y))))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   destruct x' as [ rx' | rx' sx' kx' px' | kx' px' ]; try solve [elimtype False; inv H].
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (YES' A rx sx kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (PURE' A kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   destruct y as [ ry | ry sy ky py | ky py ]; try solve [elimtype False; inv H].
   exists (NO' _ rx' n); exists (YES' _ ry sy kz pz); inv H; split; constructor; auto. simpl in *; f_equal; auto.
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (YES' A rx sx kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (PURE' A kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   destruct y as [ ry | ry sy ky py | ky py ]; try solve [elimtype False; inv H].
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
   exists (YES' _ rx' sx' kx' pz); exists (NO' _ ry n); inv H; split; constructor; auto.
(* Goal: @sigT (_functor f_res A) (fun x : _functor f_res A => @sig (_functor f_res A) (fun y0 : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 (YES' A rz sz kz pz)) (and (@eq (_functor f_res B) (@fmap f_res A B f g x) (YES' B rx' sx' kx' px')) (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g (YES' A ry sy ky py)))))) *)
(* Goal: @sigT (_functor f_res A) (fun x : _functor f_res A => @sig (_functor f_res A) (fun y0 : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 (PURE' A kz pz)) (and (@eq (_functor f_res B) (@fmap f_res A B f g x) x') (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y))))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   exists (YES' _ rx' sx' kx' pz); exists (YES' _ ry sy ky pz); inv H; split; constructor; auto; simpl; f_equal; auto.
   exists (PURE' _ kz pz); exists (PURE' _ kz pz); simpl in *; inv H; split; [constructor | tauto].

(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) x y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   destruct x as [ rx | rx sx kx px | kx px ]; try solve [elimtype False; inv H].
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (YES' A rx sx kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (PURE' A kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   destruct y as [ ry | ry sy ky py | ky py ]; try solve [elimtype False; inv H].
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (YES' A rx sx kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g (YES' A ry sy ky py))) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (PURE' A kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   destruct z' as [ rz | rz sz kz pz | kz pz ]; try solve [elimtype False; inv H].
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
   exists (NO' _ ry n0); exists (NO' _ rz n1); inv H; split; constructor; auto.
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (YES' A rx sx kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g (YES' A ry sy ky py))) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (PURE' A kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   destruct z' as [ rz | rz sz kz pz | kz pz ]; try solve [elimtype False; inv H].
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
   exists (YES' _ ry sy ky py); exists (YES' _ rz sz ky py); inv H; split; constructor; auto.
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (YES' A rx sx kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (PURE' A kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   destruct y as [ ry | ry sy ky py | ky py ]; try solve [elimtype False; inv H].
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (YES' A rx sx kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g (YES' A ry sy ky py))) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (PURE' A kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   destruct z' as [ rz | rz sz kz pz | kz pz ]; try solve [elimtype False; inv H].
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
   exists (NO' _ ry n); exists (YES' _ rz sz kx px); inv H; split; constructor; auto.
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (YES' A rx sx kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g (YES' A ry sy ky py))) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
(* Goal: @sigT (_functor f_res A) (fun y0 : _functor f_res A => @sig (_functor f_res A) (fun z : _functor f_res A => and (@join (_functor f_res A) (res_join A) (PURE' A kx px) y0 z) (and (@eq (_functor f_res B) (@fmap f_res A B f g y0) (@fmap f_res A B f g y)) (@eq (_functor f_res B) (@fmap f_res A B f g z) z')))) *)
   destruct z' as [ rz | rz sz kz pz | kz pz ]; try solve [elimtype False; inv H].
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
   exists (YES' _ ry sy kx px); exists (YES' _ rz sz kx px); inv H; split; constructor; auto. simpl; f_equal; auto.
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
   exists (PURE' _ kx px); exists (PURE' _ kx px); inv H; split; constructor; auto.
  Qed.

  Definition res_option (PRED : Type) (r: res PRED) : option (rshare * kind):=
    match r with
      | NO' _ _ => None
      | YES' sh rsh k _ => Some (readable_part rsh,k)
      | PURE' _ _ => None (* PUREs cannot be split in any interesting way, which is what valid is about. *)
    end.

  Definition ghost (PRED : Type) : Type :=
    list (option ({g: Ghost & {a: @G g | ghost.valid a}} * fpreds PRED)%type).

  Definition ghost_fmap (A B:Type) (f:A->B) (g:B->A)(x:ghost A) : ghost B :=
    fmap (flist (foption (fpair (fconst _) fpreds))) f g x.

  Lemma ff_ghost : functorFacts ghost ghost_fmap.
  Proof.
(* Goal: functorFacts ghost ghost_fmap *)
    constructor; intros; extensionality x; unfold ghost_fmap.
    - rewrite fmap_id; auto.
    - rewrite <- fmap_comp; auto.
  Qed.

  Definition f_ghost : functor := Functor ff_ghost.

  Instance preds_join PRED : Join _ := Join_equiv (fpreds PRED).

(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join b c f) (@join ghost ghost_join (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) f e)) *)
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join b c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
  Inductive ghost_elem_join : Join {g: Ghost & {a: @G g | ghost.valid a}} :=
  | elem_join_I g a b c va vb vc: join a b c ->
    ghost_elem_join (existT _ g (exist _ a va)) (existT _ g (exist _ b vb))
                    (existT _ g (exist _ c vc)).
  Existing Instance ghost_elem_join.

  Inductive ghost_join PRED : Join (ghost PRED) :=
  | ghost_join_nil_l m: ghost_join PRED nil m m
  | ghost_join_nil_r m: ghost_join PRED m nil m
  | ghost_join_cons a1 a2 m1 m2 a3 m3: join a1 a2 a3 -> ghost_join PRED m1 m2 m3 ->
      ghost_join PRED (a1 :: m1) (a2 :: m2) (a3 :: m3).
  Hint Constructors ghost_join.
  Existing Instance ghost_join.

  Lemma elem_join_inv: forall a1 a2 a3, ghost_elem_join a1 a2 a3 ->
  match a1, a2, a3 with
  | existT g1 (exist x1 _), existT g2 (exist x2 _), existT g3 (exist x3 _) =>
      exists H: g2 = g1, exists H': g3 = g1, join x1 (eq_rect _ _ x2 _ H) (eq_rect _ _ x3 _ H')
  end.
  Proof.
(* Goal: forall (a1 a2 a3 : @sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_ : ghost_elem_join a1 a2 a3), let (g1, s) := a1 in let (x1, _) := s in let (g2, s0) := a2 in let (x2, _) := s0 in let (g3, s1) := a3 in let (x3, _) := s1 in @ex (@eq Ghost g2 g1) (fun H : @eq Ghost g2 g1 => @ex (@eq Ghost g3 g1) (fun H' : @eq Ghost g3 g1 => @join (@G g1) (@Join_G g1) x1 (@eq_rect Ghost g2 (@G) x2 g1 H) (@eq_rect Ghost g3 (@G) x3 g1 H'))) *)
    inversion 1; subst.
(* Goal: @ex (@eq Ghost g g) (fun H : @eq Ghost g g => @ex (@eq Ghost g g) (fun H' : @eq Ghost g g => @join (@G g) (@Join_G g) a (@eq_rect Ghost g (@G) b g H) (@eq_rect Ghost g (@G) c g H'))) *)
    exists eq_refl, eq_refl; auto.
  Qed.

  Lemma ghost_join_inv: forall PRED m1 m2 m3, ghost_join PRED m1 m2 m3 ->
  match m1, m2 with
  | nil, _ => m3 = m2
  | _, nil => m3 = m1
  | a1 :: m1, a2 :: m2 => match m3 with nil => False
                          | a3 :: m3 => join a1 a2 a3 /\ ghost_join PRED m1 m2 m3 end
  end.
  Proof.
(* Goal: forall (PRED : Type) (m1 m2 m3 : ghost PRED) (_ : ghost_join PRED m1 m2 m3), match m1 with | nil => @eq (ghost PRED) m3 m2 | cons a1 m4 => match m2 with | nil => @eq (ghost PRED) m3 m1 | cons a2 m5 => match m3 with | nil => False | cons a3 m6 => and (@join (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds PRED))) (@Join_lower (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds PRED)) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (_functor fpreds PRED) (preds_join PRED))) a1 a2 a3) (ghost_join PRED m4 m5 m6) end end end *)
    induction 1; simpl; auto.
(* Goal: match m with | nil => @eq (ghost PRED) m (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) PRED))))) | cons a1 m1 => @eq (ghost PRED) m m end *)
    destruct m; simpl; auto.
  Qed.

  Instance pa_gej : @Perm_alg _ ghost_elem_join.
  Proof.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
    constructor.
    - inversion 1; inversion 1; subst.
(* Goal: @eq (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) a0 va)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) c vc)) *)
      inv H.
      repeat (match goal with H : existT _ _ _ = existT _ _ _ |- _ => apply inj_pair2 in H end;
          subst).
(* Goal: @eq (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) c vc)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) c1 vc0)) *)
      f_equal; eapply exist_ext, join_eq; eauto.
    - intros ????? J1%elem_join_inv J2%elem_join_inv.
      destruct a as (ga & a & ?), b as (gb & b & ?), c as (gc & c & ?), d as (gd & d & ?),
        e as (ge & e & ?).
(* Goal: @sigT (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (fun f : @sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) => and (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) gb (@exist (@G gb) (fun a : @G gb => @valid gb a) b v0)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) gc (@exist (@G gc) (fun a : @G gc => @valid gc a) c v1)) f) (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) a v)) f (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ge (@exist (@G ge) (fun a : @G ge => @valid ge a) e v3)))) *)
      repeat (apply realize_eq in J1; destruct J1 as [? J1]).
(* Goal: @sigT (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (fun f : @sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) => and (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) gb (@exist (@G gb) (fun a : @G gb => @valid gb a) b v0)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) gc (@exist (@G gc) (fun a : @G gc => @valid gc a) c v1)) f) (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) a v)) f (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ge (@exist (@G ge) (fun a : @G ge => @valid ge a) e v3)))) *)
      repeat (apply realize_eq in J2; destruct J2 as [? J2]); subst.
(* Goal: @sigT (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (fun f : @sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) => and (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) b v0)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) c v1)) f) (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) a v)) f (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) e v3)))) *)
      destruct (join_assoc J1 J2) as (f & ? & J).
(* Goal: @sigT (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (fun f : @sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) => and (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) b v0)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) c v1)) f) (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) a v)) f (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) e v3)))) *)
      exists (existT _ ga (exist _ f (join_valid _ _ _ (join_comm J) v3))).
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      split; constructor; auto.
    - inversion 1; constructor; auto.
    - inversion 1; subst; inversion 1; subst; auto.
(* Goal: @eq (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) a0 va)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) c vc)) *)
      inv H.
      repeat (match goal with H : existT _ _ _ = existT _ _ _ |- _ => apply inj_pair2 in H end;
          subst).
(* Goal: @eq (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) a0 va)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) c vc)) *)
      f_equal; eapply exist_ext, join_positivity; eauto.
  Qed.

  Instance pa_gj : forall PRED, @Perm_alg _ (ghost_join PRED).
  Proof.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
    constructor.
    - intros until 1; revert z'; induction H; inversion 1; subst; auto.
(* Goal: @eq (SM.ghost (@pred rmap ag_rmap)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap)))) a g1) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap)))) o g2) *)
      f_equal; auto.
(* Goal: @eq (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a3 a5 *)
      eapply join_eq; eauto.
    - induction a; intros ???? J1 J2; apply ghost_join_inv in J1; subst.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
      { exists e; split; auto; constructor. }
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join b c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
      destruct b; subst; [eexists; split; eauto; constructor|].
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
      destruct d; [contradiction|].
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
      destruct J1 as [Jc1 J1].
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
      apply ghost_join_inv in J2.
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
      destruct c; subst; [eexists; split; eauto; constructor; auto|].
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o1 c) f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
      destruct e; [contradiction|].
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o1 c) f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o2 e))) *)
      destruct J2 as [Jc2 J2].
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o1 c) f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o2 e))) *)
      destruct (join_assoc Jc1 Jc2) as (f & ? & ?).
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o1 c) f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o2 e))) *)
      destruct (IHa _ _ _ _ J1 J2) as (f' & ? & ?).
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      exists (f :: f'); split; constructor; auto.
    - induction 1; constructor; auto.
    - intros until 1; revert b'; induction H; inversion 1; subst; auto.
(* Goal: @eq ghost (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a1 m1) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a3 m3) *)
      f_equal; eauto.
(* Goal: @eq (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a1 a3 *)
      eapply join_positivity; eauto.
  Qed.

  Instance sa_gj : forall PRED, @Sep_alg _ (ghost_join PRED).
  Proof.
(* Goal: @Sep_alg ghost ghost_join *)
    intros; exists (fun _ => nil); auto; constructor.
  Defined.

  Opaque fpreds.

  Definition paf_ghost : @pafunctor f_ghost ghost_join.
  Proof.
(* Goal: forall x : rmap', @eq rmap' (pre_rmap2rmap' (rmap'2pre_rmap x)) x *)
    constructor; repeat intro.
    - induction H; constructor; auto.
(* Goal: @join (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Join_lower (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join preds preds_join)) (@option_map (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap))) (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (fun '(pair a b) => @pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds a (p2pred b)) a1) (@option_map (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap))) (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (fun '(pair a b) => @pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds a (p2pred b)) a2) (@option_map (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap))) (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (fun '(pair a b) => @pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds a (p2pred b)) a3) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
      inv H; constructor; auto.
(* Goal: @join (_functor (fpair (fconst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)))) fpreds) B) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (_functor fpreds B) (preds_join B)) (@fmap (fpair (fconst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)))) fpreds) A B f g a0) (@fmap (fpair (fconst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)))) fpreds) A B f g a4) (@fmap (fpair (fconst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)))) fpreds) A B f g a5) *)
      inv H1; constructor; auto.
(* Goal: @join (_functor fpreds B) (preds_join B) (@snd (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@fmap (fpair (fconst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)))) fpreds) A B f g a0)) (@snd (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@fmap (fpair (fconst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)))) fpreds) A B f g a4)) (@snd (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@fmap (fpair (fconst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)))) fpreds) A B f g a5)) *)
      inv H2; constructor; auto; simpl; congruence.
    - revert dependent z; revert y; induction x'; intros; apply ghost_join_inv in H.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
      { exists nil, z; split; auto; constructor. }
      destruct y; simpl in *.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
      { exists z, nil; split; auto; constructor. }
      destruct z; [contradiction | simpl in *].
(* Goal: @sigT (ghost A) (fun y0 : ghost A => @sig (ghost A) (fun z : ghost A => and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) a x) y0 z) (and (@eq (ghost B) (ghost_fmap A B f g y0) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) (@eq (ghost B) (ghost_fmap A B f g z) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) o0 z'))))) *)
      destruct H as [J1 J2].
(* Goal: @sigT (ghost A) (fun x : ghost A => @sig (ghost A) (fun y0 : ghost A => and (@join (ghost A) (ghost_join A) x y0 (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o0 z)) (and (@eq (ghost B) (ghost_fmap A B f g x) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) a x')) (@eq (ghost B) (ghost_fmap A B f g y0) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y)))))) *)
      destruct (IHx' _ _ J2) as (x & y' & ? & ? & ?); subst.
(* Goal: @sigT (ghost A) (fun y0 : ghost A => @sig (ghost A) (fun z0 : ghost A => and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) a x) y0 z0) (and (@eq (ghost B) (ghost_fmap A B f g y0) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) (@eq (ghost B) (ghost_fmap A B f g z0) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) o0 (ghost_fmap A B f g z)))))) *)
      apply lower_join_inv in J1.
(* Goal: @sigT (ghost A) (fun y0 : ghost A => @sig (ghost A) (fun z0 : ghost A => and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) a x) y0 z0) (and (@eq (ghost B) (ghost_fmap A B f g y0) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) (@eq (ghost B) (ghost_fmap A B f g z0) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) o0 (ghost_fmap A B f g z)))))) *)
      destruct a as [[[? []]]|].
      + destruct o as [[[? []]]|].
        * destruct o0 as [[[? []]]|]; [|contradiction].
          destruct J1 as [J1%elem_join_inv J1']; simpl in *.
          repeat (apply realize_eq in J1 as [? J1]); subst; simpl in *.
          exists (Some (existT _ x0 (exist _ _ v), _f1) :: x),
            (Some (existT _ x0 (exist _ _ v0), _f1) :: y').
(* Goal: and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) x) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y') (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o z)) (and (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y')) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o z)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) o0 (ghost_fmap A B f g z)))) *)
          split; [repeat constructor; auto|].
          unfold ghost_fmap in *; simpl in *.
(* Goal: and (@eq (ghost B) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x0 (@exist (@G x0) (@valid x0) x3 v0)) (@fmap fpreds A B f g _f))) (@map (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (fun x : option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A)) => match x with | Some x0 => @Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@fst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0) (@fmap fpreds A B f g (@snd (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0))) | None => @None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) end) y')) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x0 (@exist (@G x0) (fun a : @G x0 => @valid x0 a) x3 v0)) (@fmap fpreds A B f g _f0))) (@map (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (fun x : option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A)) => match x with | Some x0 => @Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@fst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0) (@fmap fpreds A B f g (@snd (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0))) | None => @None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) end) y))) (@eq (ghost B) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x0 (@exist (@G x0) (@valid x0) x5 v1)) (@fmap fpreds A B f g _f))) (@map (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (fun x : option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A)) => match x with | Some x0 => @Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@fst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0) (@fmap fpreds A B f g (@snd (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0))) | None => @None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) end) z)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x0 (@exist (@G x0) (fun a : @G x0 => @valid x0 a) x5 v1)) _f1)) (@map (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (fun x : option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A)) => match x with | Some x0 => @Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@fst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0) (@fmap fpreds A B f g (@snd (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0))) | None => @None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) end) z))) *)
          inv J1'.
          rewrite <- H1, <- H2; auto.
        * destruct o0 as [[[? []]]|]; [|contradiction].
(* Goal: @sigT (ghost A) (fun y0 : ghost A => @sig (ghost A) (fun z0 : ghost A => and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x0 (@exist (@G x0) (fun a : @G x0 => @valid x0 a) x1 v)) _f)) x) y0 z0) (and (@eq (ghost B) (ghost_fmap A B f g y0) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) y))) (@eq (ghost B) (ghost_fmap A B f g z0) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x2 (@exist (@G x2) (fun a : @G x2 => @valid x2 a) x3 v0)) _f0)) (ghost_fmap A B f g z)))))) *)
          inv J1.
          match goal with H : existT _ _ _ = existT _ _ _ |- _ => apply inj_pair2 in H end;
(* Goal: @join (res KSa.K.predicate) (SM.res_join KSa.K.predicate) (YES' (@pred K.knot K.ageable_knot) ra sha kc (@existT TypeTree (fun i : TypeTree => _functor (@fpi (list Type) (fun ts : list Type => dependent_type_functor_rec ts i)) (@pred K.knot K.ageable_knot)) x1 p)) (YES' (@pred K.knot K.ageable_knot) rb shb kc (@existT TypeTree (fun i : TypeTree => _functor (@fpi (list Type) (fun ts : list Type => dependent_type_functor_rec ts i)) (@pred K.knot K.ageable_knot)) x1 p)) (YES' (@pred K.knot K.ageable_knot) rc shc kc (@existT TypeTree (fun i : TypeTree => _functor (@fpi (list Type) (fun ts : list Type => dependent_type_functor_rec ts i)) (@pred K.knot K.ageable_knot)) x1 p)) *)
            subst.
(* Goal: @sigT (ghost A) (fun x0 : ghost A => @sig (ghost A) (fun y0 : ghost A => and (@join (ghost A) (ghost_join A) x0 y0 (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x2 (@exist (@G x2) (fun a : @G x2 => @valid x2 a) x3 v0)) _f0)) z)) (and (@eq (ghost B) (ghost_fmap A B f g x0) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x2 (@exist (@G x2) (fun a : @G x2 => @valid x2 a) x3 v)) (@fmap fpreds A B f g _f0))) (ghost_fmap A B f g x))) (@eq (ghost B) (ghost_fmap A B f g y0) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) y)))))) *)
          exists (Some (existT _ x2 (exist _ _ v0), _f0) :: x), (None :: y').
(* Goal: and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) x) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y') (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o z)) (and (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y')) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o z)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) o0 (ghost_fmap A B f g z)))) *)
          split; [repeat constructor; auto|].
          unfold ghost_fmap in *; simpl in *.
          rewrite <- H1; split; f_equal; f_equal; f_equal; f_equal.
(* Goal: @eq (@sig (@G x2) (@valid x2)) (@exist (@G x2) (@valid x2) x3 v) (@exist (@G x2) (fun a : @G x2 => @valid x2 a) x3 v0) *)
          apply exist_ext; auto.
      + exists (None :: x), (o0 :: y').
(* Goal: and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) x) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y') (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o z)) (and (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y')) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o z)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) o0 (ghost_fmap A B f g z)))) *)
        split; [repeat constructor; auto|].
(* Goal: and (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) x)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (ghost_fmap A B f g x))) (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o0 y')) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) *)
        split; auto.
        unfold ghost_fmap in *; simpl in *.
        rewrite <- H1; f_equal.
(* Goal: @eq (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) match o0 with | Some x0 => @Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@fst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0) (@fmap fpreds A B f g (@snd (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0))) | None => @None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) end match o with | Some x0 => @Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@fst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0) (@fmap fpreds A B f g (@snd (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0))) | None => @None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) end *)
        destruct o, o0; inv J1; auto.
    - revert dependent z'; revert y; induction x; intros; apply ghost_join_inv in H; simpl in H.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
      { exists y, y; split; auto; constructor. }
      destruct y; simpl in *.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
      { exists nil, (a :: x); split; auto; constructor. }
      destruct z'; [contradiction | simpl in *].
(* Goal: @sigT (ghost A) (fun y0 : ghost A => @sig (ghost A) (fun z : ghost A => and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) a x) y0 z) (and (@eq (ghost B) (ghost_fmap A B f g y0) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) (@eq (ghost B) (ghost_fmap A B f g z) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) o0 z'))))) *)
      destruct H as [J1 J2].
(* Goal: @sigT (ghost A) (fun y0 : ghost A => @sig (ghost A) (fun z : ghost A => and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) a x) y0 z) (and (@eq (ghost B) (ghost_fmap A B f g y0) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) (@eq (ghost B) (ghost_fmap A B f g z) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) o0 z'))))) *)
      destruct (IHx _ _ J2) as (y' & z & ? & ? & ?); subst.
(* Goal: @sigT (ghost A) (fun y0 : ghost A => @sig (ghost A) (fun z0 : ghost A => and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) a x) y0 z0) (and (@eq (ghost B) (ghost_fmap A B f g y0) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) (@eq (ghost B) (ghost_fmap A B f g z0) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) o0 (ghost_fmap A B f g z)))))) *)
      apply lower_join_inv in J1.
(* Goal: @sigT (ghost A) (fun y0 : ghost A => @sig (ghost A) (fun z0 : ghost A => and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) a x) y0 z0) (and (@eq (ghost B) (ghost_fmap A B f g y0) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) (@eq (ghost B) (ghost_fmap A B f g z0) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) o0 (ghost_fmap A B f g z)))))) *)
      destruct a as [[[? []]]|].
      + destruct o as [[[? []]]|].
        * destruct o0 as [[[? []]]|]; [|contradiction].
          destruct J1 as [J1%elem_join_inv J1']; simpl in *.
          repeat (apply realize_eq in J1 as [? J1]); subst; simpl in *.
          exists (Some (existT _ x0 (exist _ _ v0), _f) :: y'),
            (Some (existT _ x0 (exist _ _ v1), _f) :: z).
(* Goal: and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) x) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y') (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o z)) (and (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y')) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o z)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) o0 (ghost_fmap A B f g z)))) *)
          split; [repeat constructor; auto|].
          unfold ghost_fmap in *; simpl in *.
(* Goal: and (@eq (ghost B) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x0 (@exist (@G x0) (@valid x0) x3 v0)) (@fmap fpreds A B f g _f))) (@map (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (fun x : option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A)) => match x with | Some x0 => @Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@fst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0) (@fmap fpreds A B f g (@snd (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0))) | None => @None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) end) y')) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x0 (@exist (@G x0) (fun a : @G x0 => @valid x0 a) x3 v0)) (@fmap fpreds A B f g _f0))) (@map (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (fun x : option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A)) => match x with | Some x0 => @Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@fst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0) (@fmap fpreds A B f g (@snd (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0))) | None => @None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) end) y))) (@eq (ghost B) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x0 (@exist (@G x0) (@valid x0) x5 v1)) (@fmap fpreds A B f g _f))) (@map (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (fun x : option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A)) => match x with | Some x0 => @Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@fst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0) (@fmap fpreds A B f g (@snd (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0))) | None => @None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) end) z)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x0 (@exist (@G x0) (fun a : @G x0 => @valid x0 a) x5 v1)) _f1)) (@map (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (fun x : option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A)) => match x with | Some x0 => @Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@fst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0) (@fmap fpreds A B f g (@snd (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0))) | None => @None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) end) z))) *)
          inv J1'.
          rewrite <- H0, <- H1; auto.
        * destruct o0 as [[[? []]]|]; [|contradiction].
(* Goal: @sigT (ghost A) (fun y0 : ghost A => @sig (ghost A) (fun z0 : ghost A => and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x0 (@exist (@G x0) (fun a : @G x0 => @valid x0 a) x1 v)) _f)) x) y0 z0) (and (@eq (ghost B) (ghost_fmap A B f g y0) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) y))) (@eq (ghost B) (ghost_fmap A B f g z0) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x2 (@exist (@G x2) (fun a : @G x2 => @valid x2 a) x3 v0)) _f0)) (ghost_fmap A B f g z)))))) *)
          inv J1.
          match goal with H : existT _ _ _ = existT _ _ _ |- _ => apply inj_pair2 in H end;
(* Goal: @join (res KSa.K.predicate) (SM.res_join KSa.K.predicate) (YES' (@pred K.knot K.ageable_knot) ra sha kc (@existT TypeTree (fun i : TypeTree => _functor (@fpi (list Type) (fun ts : list Type => dependent_type_functor_rec ts i)) (@pred K.knot K.ageable_knot)) x1 p)) (YES' (@pred K.knot K.ageable_knot) rb shb kc (@existT TypeTree (fun i : TypeTree => _functor (@fpi (list Type) (fun ts : list Type => dependent_type_functor_rec ts i)) (@pred K.knot K.ageable_knot)) x1 p)) (YES' (@pred K.knot K.ageable_knot) rc shc kc (@existT TypeTree (fun i : TypeTree => _functor (@fpi (list Type) (fun ts : list Type => dependent_type_functor_rec ts i)) (@pred K.knot K.ageable_knot)) x1 p)) *)
            subst.
(* Goal: @sigT (ghost A) (fun y0 : ghost A => @sig (ghost A) (fun z0 : ghost A => and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x2 (@exist (@G x2) (fun a : @G x2 => @valid x2 a) x3 v)) _f)) x) y0 z0) (and (@eq (ghost B) (ghost_fmap A B f g y0) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) y))) (@eq (ghost B) (ghost_fmap A B f g z0) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) x2 (@exist (@G x2) (fun a : @G x2 => @valid x2 a) x3 v0)) (@fmap fpreds A B f g _f))) (ghost_fmap A B f g z)))))) *)
          exists (None :: y'), (Some (existT _ x2 (exist _ _ v), _f) :: z).
(* Goal: and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) x) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y') (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o z)) (and (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y')) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o z)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) o0 (ghost_fmap A B f g z)))) *)
          split; [repeat constructor; auto|].
          unfold ghost_fmap in *; simpl in *.
          rewrite <- H0; split; f_equal; f_equal; f_equal; f_equal.
(* Goal: @eq (@sig (@G x2) (@valid x2)) (@exist (@G x2) (@valid x2) x3 v) (@exist (@G x2) (fun a : @G x2 => @valid x2 a) x3 v0) *)
          apply exist_ext; auto.
      + exists (o :: y'), (o :: z).
(* Goal: and (@join (ghost A) (ghost_join A) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) x) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y') (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o z)) (and (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y')) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o z)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) o0 (ghost_fmap A B f g z)))) *)
        split; [repeat constructor; auto|].
        unfold ghost_fmap in *; simpl in *; rewrite <- H0; split; f_equal.
(* Goal: @eq (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) match o with | Some x0 => @Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B) (@fst (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0) (@fmap fpreds A B f g (@snd (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A) x0))) | None => @None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B)) end o0 *)
        destruct o, o0; auto; contradiction.
  Qed.

  Definition pre_rmap (A:Type) := ((address -> res A) * ghost A)%type.
  Definition f_pre_rmap : functor :=
    fpair (ffunc (fconst address) f_res) f_ghost.

  Notation Join_obj A := (Join_prod _ (Join_fun address (res A) (res_join A)) _ (ghost_join A)).

  Instance Join_pre_rmap (A: Type) : Join (pre_rmap A) :=
    Join_obj A.

  Definition paf_pre_rmap : @pafunctor f_pre_rmap Join_pre_rmap :=
    paf_pair (paf_fun address paf_res) paf_ghost.

  Definition Perm_pre_rmap (A: Type): Perm_alg (pre_rmap A) :=
    Perm_prod (Perm_fun address _ _ _) (pa_gj A).

  Definition Sep_pre_rmap (A: Type): Sep_alg (pre_rmap A) :=
    Sep_prod (Sep_fun address _ _ _) (sa_gj A).

Lemma pre_rmap_core:
forall (A : Type) (m : f_pre_rmap A),
  @core (f_pre_rmap A) (Join_pre_rmap A) (Sep_pre_rmap A) m =
 (@core ((fpair (ffunc (fconst address) f_res) f_ghost) A)
           (Join_prod ((ffunc (fconst address) f_res) A)
              (Join_pi ((fconst address) A)
                 (fun _ : (fconst address) A => f_res A)
                 (fun _ : (fconst address) A => Join_res A))
              (f_ghost A) (ghost_join A))
           (@Sep_prod ((ffunc (fconst address) f_res) A)
              (Join_pi ((fconst address) A)
                 (fun _ : (fconst address) A => f_res A)
                 (fun _ : (fconst address) A => Join_res A))
              (f_ghost A) (ghost_join A)
              (Sep_pi ((fconst address) A)
                 (fun _ : (fconst address) A => f_res A)
                 (fun _ : (fconst address) A => Join_res A)
                 (fun _ : (fconst address) A => sa_rj A)) 
              (sa_gj A)) m).
Proof.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
intros. reflexivity.
Qed.

End StratModel.

Local Open Scope nat_scope.

Module Type RMAPS.
  Declare Module AV:ADR_VAL.
  Import AV.

  Parameter rmap : Type.
  Axiom Join_rmap: Join rmap. Existing Instance Join_rmap.
  Axiom Perm_rmap: Perm_alg rmap. Existing Instance Perm_rmap.
  Axiom Sep_rmap: Sep_alg rmap. Existing Instance Sep_rmap.
  Axiom ag_rmap: ageable rmap.  Existing Instance ag_rmap.
  Axiom Age_rmap: Age_alg rmap.  Existing Instance Age_rmap.

  Inductive preds : Type :=
    SomeP : forall A : TypeTree,
      (forall ts: list Type, dependent_type_functor_rec ts A (pred rmap)) -> preds.

  Definition NoneP := SomeP (ConstType unit) (fun _ => tt).

  Inductive resource : Type :=
    | NO: forall sh: Share.t, ~(readable_share sh) -> resource
    | YES: forall sh: Share.t, readable_share sh -> kind -> preds -> resource
    | PURE: kind -> preds -> resource.

  Definition res_option (r:resource) : option (rshare * kind) :=
    match r with
      | NO _ _ => None
      | YES sh rsh k _ => Some (readable_part rsh,k)
      | PURE k _ => None
    end.

  Inductive res_join : resource -> resource -> resource -> Prop :=
   | res_join_NO1 : forall sh1 nsh1 sh2 nsh2 sh3 nsh3
                 (RJ: join sh1 sh2 sh3),
                 res_join (NO sh1 nsh1) (NO sh2 nsh2) (NO sh3 nsh3)
   | res_join_NO2 : forall sh1 rsh1 sh2 nsh2 sh3 rsh3 k p
                 (RJ: join sh1 sh2 sh3), 
                 res_join (YES sh1 rsh1 k p) (NO sh2 nsh2) (YES sh3 rsh3 k p) 
   | res_join_NO3 : forall sh1 nsh1 sh2 rsh2 sh3 rsh3 k p
                 (RJ: join sh1 sh2 sh3),
                 res_join (NO sh1 nsh1) (YES sh2 rsh2 k p) (YES sh3 rsh3 k p) 
   | res_join_YES : forall sh1 rsh1 sh2 rsh2 sh3 rsh3 k p
                 (RJ: join sh1 sh2 sh3),
        res_join (YES sh1 rsh1 k p) (YES sh2 rsh2 k p) (YES sh3 rsh3 k p)
   | res_join_PURE : forall k p, res_join (PURE k p) (PURE k p) (PURE k p). 

  Instance Join_resource: Join resource := res_join.
  Axiom Perm_resource: Perm_alg resource. Existing Instance Perm_resource.
  Axiom Sep_resource: Sep_alg resource. Existing Instance Sep_resource.

  Definition preds_fmap (f g: pred rmap -> pred rmap) (x:preds) : preds :=
    match x with SomeP A Q => SomeP A (fmap (fpi _) f g Q)
    end.
  (* Check whether the following two can be erased. *)
  Axiom preds_fmap_id : preds_fmap (id _) (id _) = id preds.
  Axiom preds_fmap_comp : forall f1 f2 g1 g2,
    preds_fmap g1 g2 oo preds_fmap f1 f2 = preds_fmap (g1 oo f1) (f2 oo g2).

  Definition resource_fmap (f g:pred rmap -> pred rmap) (x:resource) : resource :=
    match x with
    | NO sh nsh => NO sh nsh
    | YES sh rsh k p => YES sh rsh k (preds_fmap f g p)
    | PURE k p => PURE k (preds_fmap f g p)
    end.
  Axiom resource_fmap_id : resource_fmap (id _) (id _) = id resource.
  Axiom resource_fmap_comp : forall f1 f2 g1 g2,
    resource_fmap g1 g2 oo resource_fmap f1 f2 = resource_fmap (g1 oo f1) (f2 oo g2).

  Definition ghost : Type := list (option ({g: Ghost & {a: @G g | ghost.valid a}} * preds)%type).

  Instance preds_join : Join _ := Join_equiv preds.

(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join b c f) (@join ghost ghost_join (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) f e)) *)
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join b c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
  Inductive ghost_elem_join : Join {g: Ghost & {a: @G g | ghost.valid a}} :=
  | elem_join_I g a b c va vb vc: join a b c ->
    ghost_elem_join (existT _ g (exist _ a va)) (existT _ g (exist _ b vb))
                    (existT _ g (exist _ c vc)).
  Existing Instance ghost_elem_join.

  Inductive ghost_join : Join ghost :=
  | ghost_join_nil_l m: ghost_join nil m m
  | ghost_join_nil_r m: ghost_join m nil m
  | ghost_join_cons a1 a2 m1 m2 a3 m3: join a1 a2 a3 -> ghost_join m1 m2 m3 ->
      ghost_join (a1 :: m1) (a2 :: m2) (a3 :: m3).
  Existing Instance ghost_join.

  Axiom Perm_ghost: Perm_alg ghost. Existing Instance Perm_ghost.
  Axiom Sep_ghost: Sep_alg ghost. Existing Instance Sep_ghost.
  Axiom ghost_core: forall (g: ghost), core g = nil.

  Definition ghost_fmap (f g:pred rmap -> pred rmap)(x:ghost) : ghost :=
    map (option_map (fun '(a, b) => (a, preds_fmap f g b))) x.

  Axiom ghost_fmap_id : ghost_fmap (id _) (id _) = id ghost.
  Axiom ghost_fmap_comp : forall f1 f2 g1 g2,
    ghost_fmap g1 g2 oo ghost_fmap f1 f2 = ghost_fmap (g1 oo f1) (f2 oo g2).

  Definition rmap' := ((address -> resource) * ghost)%type.

  Definition rmap_fmap (f g: pred rmap -> pred rmap) (x:rmap') : rmap' :=
    (resource_fmap f g oo fst x, ghost_fmap f g (snd x)).

  Axiom rmap_fmap_id : rmap_fmap (id _) (id _) = id rmap'.
  Axiom rmap_fmap_comp : forall f1 f2 g1 g2,
   rmap_fmap g1 g2 oo rmap_fmap f1 f2 = rmap_fmap (g1 oo f1) (f2 oo g2).

  Parameter squash : (nat * rmap') -> rmap.
  Parameter unsquash : rmap -> (nat * rmap').


  Axiom rmap_level_eq: @level rmap _ = fun x => fst (unsquash x).
  Axiom rmap_age1_eq: @age1 _ _ =
     fun k => match unsquash k with
    | (O,_) => None
    | (S n,x) => Some (squash (n,x))
    end.

  Definition resource_at (phi:rmap) : address -> resource := fst (snd (unsquash phi)).
  Infix "@" := resource_at (at level 50, no associativity).
  Definition ghost_of (phi:rmap) : ghost := snd (snd (unsquash phi)).

  Instance Join_nat_rmap': Join (nat * rmap') := Join_prod _ (Join_equiv nat) _ _.

  Axiom join_unsquash : forall phi1 phi2 phi3,
    join phi1 phi2 phi3 <->
    join (unsquash phi1) (unsquash phi2) (unsquash phi3).

  Definition rmap_unage (k:rmap) : rmap :=
    match unsquash k with
    | (n,x) => squash (S n, x)
    end.

  Program Definition approx (n:nat) (p: pred rmap) : pred rmap :=
    fun w => level w < n /\ p w.
  Next Obligation.
(* Goal: and (lt (@level rmap ag_rmap a') n) (@app_pred rmap ag_rmap p a') *)
  destruct H0.
(* Goal: and (lt (@level rmap ag_rmap a') n) (@app_pred rmap ag_rmap p a') *)
  split.
(* Goal: lt (@level rmap ag_rmap a') n *)
(* Goal: @app_pred rmap ag_rmap p a' *)
  apply age_level in H. omega.
(* Goal: @app_pred rmap ag_rmap p a' *)
  apply pred_hereditary with a; auto.
  Qed.

  Axiom squash_unsquash : forall phi, squash (unsquash phi) = phi.
  Axiom unsquash_squash : forall n rm, unsquash (squash (n,rm)) = (n,rmap_fmap (approx n) (approx n) rm).
  Axiom ghost_of_core : forall phi, ghost_of (core phi) = core (ghost_of phi).

End RMAPS.

Module Rmaps (AV':ADR_VAL): RMAPS with Module AV:=AV'.
  Module AV:=AV'.
  Import AV.

  Module SM := StratModel(AV).
  Import SM.

  Module TyF. (* <: TY_FUNCTOR_PROP. *)
    Definition F := f_pre_rmap.
  End TyF.

  Module TyFSA <: KNOT_FULL_SA_INPUT with Module KI:=TyF.
    Module KI := TyF.
    Import KI.

    Instance Join_F: forall A, Join (F A) := _.
    Definition Perm_F : forall A, Perm_alg (F A) := Perm_pre_rmap.
    Definition Sep_F := Sep_pre_rmap.
    Definition paf_F := paf_pre_rmap.
  End TyFSA.

  Module K := Knot_MixVariantHeredProp(TyF).
  Module KL := KnotLemmas_MixVariantHeredProp(K).
  Module KSa := KnotFullSa(TyFSA)(K)(KL).

  Definition rmap := K.knot.
  Instance Join_rmap: Join rmap := KSa.Join_knot.
  Instance Perm_rmap : Perm_alg rmap:= KSa.Perm_knot.
  Instance Sep_rmap : Sep_alg rmap:= KSa.Sep_knot.
  Instance ag_rmap : ageable rmap := K.ageable_knot.
  Instance Age_rmap: Age_alg rmap := KSa.asa_knot.

  Inductive preds : Type :=
    SomeP : forall A : TypeTree,
    (forall ts: list Type, dependent_type_functor_rec ts A (pred rmap)) -> preds.

  Definition NoneP := SomeP (ConstType unit) (fun _ => tt).

  Inductive resource : Type :=
    | NO: forall sh: Share.t, ~ readable_share sh -> resource
    | YES: forall sh: Share.t, readable_share sh -> kind -> preds -> resource
    | PURE: kind -> preds -> resource.

  Definition resource2res (r: resource): res (pred rmap) :=
    match r with
      | NO sh nsh => NO' (pred rmap) sh nsh
      | YES sh rsh k (SomeP A l) => YES' (pred rmap) sh rsh k (existT _ A l)
      | PURE k (SomeP A l) => PURE' (pred rmap) k (existT _ A l)
    end.

  Definition res2resource (r: res (pred rmap)) : resource :=
    match r with
      | NO' sh nsh => NO sh nsh
      | YES' sh rsh k (existT A l) => YES sh rsh k (SomeP A l)
      | PURE' k (existT A l) => PURE k (SomeP A l)
    end.

  Lemma res2resource2res: forall x, resource2res (res2resource x) = x.
  Proof. unfold resource2res, res2resource; destruct x as [? | ? ? ? [? ?] | ? [? ?]]; auto. Qed.

  Lemma resource2res2resource: forall x, res2resource (resource2res x) = x.
  Proof. unfold resource2res, res2resource; destruct x; try destruct p0; try destruct p; auto. Qed.

  Definition res_option (r:resource) : option (rshare * kind) :=
    match r with
      | NO _ _ => None
      | YES sh rsh k _ => Some (readable_part rsh,k)
      | PURE k _ => None
    end.

  Lemma res_option_rewrite: res_option = SM.res_option (pred rmap) oo resource2res.
  Proof.
(* Goal: @eq (forall _ : resource, option (prod rshare kind)) res_option (@compose resource (res (@pred rmap ag_rmap)) (option (prod rshare AV.kind)) (SM.res_option (@pred rmap ag_rmap)) resource2res) *)
    unfold SM.res_option, res_option, compose.
(* Goal: @eq (forall _ : resource, option (prod rshare kind)) (fun r : resource => match r with | NO sh n => @None (prod rshare kind) | YES sh rsh k p => @Some (prod rshare kind) (@pair rshare kind (@readable_part sh rsh) k) | PURE k p => @None (prod rshare kind) end) (fun x : resource => match resource2res x with | @NO' _ sh n => @None (prod rshare AV.kind) | @YES' _ sh rsh k _f => @Some (prod rshare AV.kind) (@pair rshare AV.kind (@readable_part sh rsh) k) | @PURE' _ k _f => @None (prod rshare AV.kind) end) *)
    extensionality r; destruct r; simpl; auto; destruct p; auto.
  Qed.

  Definition ghost : Type := list (option ({g: Ghost & {a: @G g | ghost.valid a}} * preds)%type).

  Definition pred2p (p: preds) : fpreds (pred rmap) :=
    match p with SomeP A P => existT _ A P end.

  Definition p2pred (p: fpreds (pred rmap)) : preds :=
    match p with existT A P => SomeP A P end.

  Definition ghost2g (r: ghost): SM.ghost (pred rmap) :=
    map (option_map (fun '(a, b) => (a, pred2p b))) r.

  Definition g2ghost (r: SM.ghost (pred rmap)) : ghost :=
    map (option_map (fun '(a, b) => (a, p2pred b))) r.

  Lemma g2ghost2g: forall x, ghost2g (g2ghost x) = x.
  Proof.
(* Goal: forall x : ghost, @eq ghost (g2ghost (ghost2g x)) x *)
    induction x; auto; simpl.
(* Goal: @eq ghost (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@option_map (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (fun '(pair a b) => @pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds a (preds_fmap (id (@pred rmap ag_rmap)) (id (@pred rmap ag_rmap)) b)) a) (ghost_fmap (id (@pred rmap ag_rmap)) (id (@pred rmap ag_rmap)) x)) (id ghost (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a x)) *)
    rewrite IHx; destruct a as [[]|]; auto; simpl.
(* Goal: @eq (SM.ghost (@pred rmap ag_rmap)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred rmap ag_rmap))))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred rmap ag_rmap)))) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred rmap ag_rmap))) s (pred2p (p2pred _f)))) x) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred rmap ag_rmap))))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred rmap ag_rmap)))) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred rmap ag_rmap))) s _f)) x) *)
    destruct _f; auto.
  Qed.

  Lemma ghost2g2ghost: forall x, g2ghost (ghost2g x) = x.
  Proof.
(* Goal: forall x : ghost, @eq ghost (g2ghost (ghost2g x)) x *)
    induction x; auto; simpl.
(* Goal: @eq ghost (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@option_map (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (fun '(pair a b) => @pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds a (preds_fmap (id (@pred rmap ag_rmap)) (id (@pred rmap ag_rmap)) b)) a) (ghost_fmap (id (@pred rmap ag_rmap)) (id (@pred rmap ag_rmap)) x)) (id ghost (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a x)) *)
    rewrite IHx; destruct a as [[]|]; auto; simpl.
(* Goal: @eq ghost (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds s (p2pred (pred2p p)))) x) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds s p)) x) *)
    destruct p; auto.
  Qed.

  Inductive res_join : resource -> resource -> resource -> Prop :=
   | res_join_NO1 : forall sh1 nsh1 sh2 nsh2 sh3 nsh3
                 (RJ: join sh1 sh2 sh3),
                 res_join (NO sh1 nsh1) (NO sh2 nsh2) (NO sh3 nsh3)
   | res_join_NO2 : forall sh1 rsh1 sh2 nsh2 sh3 rsh3 k p
                 (RJ: join sh1 sh2 sh3), 
                 res_join (YES sh1 rsh1 k p) (NO sh2 nsh2) (YES sh3 rsh3 k p) 
   | res_join_NO3 : forall sh1 nsh1 sh2 rsh2 sh3 rsh3 k p
                 (RJ: join sh1 sh2 sh3),
                 res_join (NO sh1 nsh1) (YES sh2 rsh2 k p) (YES sh3 rsh3 k p) 
   | res_join_YES : forall sh1 rsh1 sh2 rsh2 sh3 rsh3 k p
                 (RJ: join sh1 sh2 sh3),
        res_join (YES sh1 rsh1 k p) (YES sh2 rsh2 k p) (YES sh3 rsh3 k p)
   | res_join_PURE : forall k p, res_join (PURE k p) (PURE k p) (PURE k p).

  Instance Join_resource: Join resource := res_join.
  Instance Perm_resource: Perm_alg resource.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
  Proof. constructor.
  * (*saf_eq *)
      intros x y z z' H1 H2; inv H1; inv H2;
      repeat match goal with H: join ?A ?B _, H': join ?A ?B ?C |- _ => pose proof (join_eq H H'); subst C end;
(* Goal: @eq nat n n *)
      repeat proof_irr; auto.
  * (* saf_assoc *)
(* Goal: forall (a b c d e : resource) (_ : @join resource Join_resource a b d) (_ : @join resource Join_resource d c e), @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      intros a b c d e H1 H2.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct d as [rd | rd sd kd pd | kd pd].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct a as [ra | | ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource (NO ra n0) f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct b as [rb| | ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (NO rb n1) c f) (@join resource Join_resource (NO ra n0) f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (join ra rb rd) by (inv H1; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct c as [rc | rc sc kc pc | kc pc]; try solve [elimtype False; inv H2].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct e as [re | re se ke pe | ke pe]; try solve [elimtype False; inv H2].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (NO rb n1) (YES rc sc kc pc) f) (@join resource Join_resource (NO ra n0) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (join rd rc re) by (inv H2; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      exists (NO rf (join_unreadable_shares H3 n1 n2)); split; constructor; auto.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct e as [re | re se ke pe | ke pe]; try solve [elimtype False; inv H2].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (NO rb n1) (YES rc sc kc pc) f) (@join resource Join_resource (NO ra n0) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (join rd rc re) by (inv H2; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (NO rb n) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      exists (YES rf (join_readable2 H3 sc) kc pc).
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc kc pc) (YES rf (@join_readable2 rb rc rf H3 sc) kc pc)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) kc pc) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      inv H2. split; constructor; auto.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct c as [rc | rc sc kc pc | kc pc]; try solve [elimtype False; inv H2].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct e as [re | re se ke pe | ke pe]; try solve [elimtype False; inv H2].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H0: join rd rc re) by (inv H2; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct a as [ra | ra sa ka pa | ka pa ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (NO rc n) f) (@join resource Join_resource (NO ra n0) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (NO rc n) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct b as [ | rb sb kb pb | ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H: join ra rb rd) by (inv H1; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      exists (YES rf (join_readable1 H3 sb) kd pd).  inv H1; inv H2; split; constructor; auto.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct b as [ rb | rb sb kb pb | ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H: join ra rb rd) by (inv H1; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      exists (NO rf (join_unreadable_shares H3 n0 n)).  inv H1; inv H2; split; constructor; auto.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H: join ra rb rd) by (inv H1; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      exists (YES rf (join_readable1 H3 sb) kb pb).  inv H1; inv H2; split; constructor; auto.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct e as [re | re se ke pe | ke pe]; try solve [elimtype False; inv H2].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H0: join rd rc re) by (inv H2; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct b as [ rb | rb sb kb pb | ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct a as [ra | ra sa ka pa | ka pa ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H: join ra rb rd) by (inv H1; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      exists (YES rf (join_readable2 H3 sc) kc pc).  inv H1; inv H2; split; constructor; auto.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource a f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct a as [ra | ra sa ka pa | ka pa ]; try solve [elimtype False; inv H1].
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H: join ra rb rd) by (inv H1; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) (YES rf (@join_readable1 rb rc rf H3 sb) kb pb)) (@join resource Join_resource (YES ra sa ka pa) (YES rf (@join_readable1 rb rc rf H3 sb) kb pb) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      exists (YES rf (join_readable1 H3 sb) kb pb).  inv H1; inv H2; split; try constructor; auto.
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      assert (H: join ra rb rd) by (inv H1; auto).
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) f) (@join resource Join_resource (YES ra sa ka pa) f (YES re se ke pe))) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      destruct (join_assoc H H0) as [rf [? ?]].
(* Goal: and (@join resource Join_resource (YES rb sb kb pb) (YES rc sc kc pc) (YES rf (@join_readable1 rb rc rf H3 sb) kb pb)) (@join resource Join_resource (YES ra sa ka pa) (YES rf (@join_readable1 rb rc rf H3 sb) kb pb) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      exists (YES rf (join_readable1 H3 sb) kb pb).  inv H1; inv H2; split; try constructor; auto.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
      exists (PURE kd pd). inv H1; inv H2; split; constructor.

*      (* saf_com *)
(* Goal: @eq nat n n *)
      intros a b c H; inv H; econstructor;  apply join_comm; auto.

*     (* saf_positivity *)
     intros; inv H; inv H0; 
      repeat match goal with H: join ?A ?B ?C, H': join ?C ?D ?A |- _ => 
                    pose proof (join_positivity H H'); subst C 
      end; 
(* Goal: @eq nat n n *)
      repeat proof_irr; auto.
 Qed.

  Instance Sep_resource: Sep_alg resource.
  Proof.
  apply mkSep 
    with (fun x => match x 
                   with NO _ _ => NO Share.bot bot_unreadable
                      | YES _ _ _ _ => NO Share.bot bot_unreadable
                      | PURE k pds => PURE k pds end).
(* Goal: forall x : rmap', @eq rmap' (pre_rmap2rmap' (rmap'2pre_rmap x)) x *)
  intro. destruct t; constructor; try apply join_unit1; auto.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
  intros. inversion H; auto.
  Defined.

  (* Will this give us the higher-order ghost state we want? *)
  Instance preds_join : Join _ := Join_equiv preds.

(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join b c f) (@join ghost ghost_join (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) f e)) *)
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join b c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
  Inductive ghost_elem_join : Join {g: Ghost & {a: @G g | ghost.valid a}} :=
  | elem_join_I g a b c va vb vc: join a b c ->
    ghost_elem_join (existT _ g (exist _ a va)) (existT _ g (exist _ b vb))
                    (existT _ g (exist _ c vc)).
  Existing Instance ghost_elem_join.

  Inductive ghost_join : Join ghost :=
  | ghost_join_nil_l m: ghost_join nil m m
  | ghost_join_nil_r m: ghost_join m nil m
  | ghost_join_cons a1 a2 m1 m2 a3 m3: join a1 a2 a3 -> ghost_join m1 m2 m3 ->
      ghost_join (a1 :: m1) (a2 :: m2) (a3 :: m3).
  Existing Instance ghost_join.

  Lemma elem_join_inv: forall a1 a2 a3, ghost_elem_join a1 a2 a3 ->
  match a1, a2, a3 with
  | existT g1 (exist x1 _), existT g2 (exist x2 _), existT g3 (exist x3 _) =>
      exists H: g2 = g1, exists H': g3 = g1, join x1 (eq_rect _ _ x2 _ H) (eq_rect _ _ x3 _ H')
  end.
  Proof.
(* Goal: forall (a1 a2 a3 : @sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_ : ghost_elem_join a1 a2 a3), let (g1, s) := a1 in let (x1, _) := s in let (g2, s0) := a2 in let (x2, _) := s0 in let (g3, s1) := a3 in let (x3, _) := s1 in @ex (@eq Ghost g2 g1) (fun H : @eq Ghost g2 g1 => @ex (@eq Ghost g3 g1) (fun H' : @eq Ghost g3 g1 => @join (@G g1) (@Join_G g1) x1 (@eq_rect Ghost g2 (@G) x2 g1 H) (@eq_rect Ghost g3 (@G) x3 g1 H'))) *)
    inversion 1; subst.
(* Goal: @ex (@eq Ghost g g) (fun H : @eq Ghost g g => @ex (@eq Ghost g g) (fun H' : @eq Ghost g g => @join (@G g) (@Join_G g) a (@eq_rect Ghost g (@G) b g H) (@eq_rect Ghost g (@G) c g H'))) *)
    exists eq_refl, eq_refl; auto.
  Qed.

  Lemma ghost_join_inv: forall m1 m2 m3, ghost_join m1 m2 m3 ->
  match m1, m2 with
  | nil, _ => m3 = m2
  | _, nil => m3 = m1
  | a1 :: m1, a2 :: m2 => match m3 with nil => False
                          | a3 :: m3 => join a1 a2 a3 /\ ghost_join m1 m2 m3 end
  end.
  Proof.
(* Goal: forall (PRED : Type) (m1 m2 m3 : ghost PRED) (_ : ghost_join PRED m1 m2 m3), match m1 with | nil => @eq (ghost PRED) m3 m2 | cons a1 m4 => match m2 with | nil => @eq (ghost PRED) m3 m1 | cons a2 m5 => match m3 with | nil => False | cons a3 m6 => and (@join (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds PRED))) (@Join_lower (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds PRED)) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (_functor fpreds PRED) (preds_join PRED))) a1 a2 a3) (ghost_join PRED m4 m5 m6) end end end *)
    induction 1; simpl; auto.
(* Goal: match m with | nil => @eq (ghost PRED) m (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) PRED))))) | cons a1 m1 => @eq (ghost PRED) m m end *)
    destruct m; simpl; auto.
  Qed.

  Instance pa_gej : @Perm_alg _ ghost_elem_join.
  Proof.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
    constructor.
    - inversion 1; inversion 1; subst.
(* Goal: @eq (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) a0 va)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) c vc)) *)
      inv H.
      repeat (match goal with H : existT _ _ _ = existT _ _ _ |- _ => apply inj_pair2 in H end;
          subst).
(* Goal: @eq (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) c vc)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) c1 vc0)) *)
      f_equal; eapply exist_ext, join_eq; eauto.
    - intros ????? J1%elem_join_inv J2%elem_join_inv.
      destruct a as (ga & a & ?), b as (gb & b & ?), c as (gc & c & ?), d as (gd & d & ?),
        e as (ge & e & ?).
(* Goal: @sigT (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (fun f : @sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) => and (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) gb (@exist (@G gb) (fun a : @G gb => @valid gb a) b v0)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) gc (@exist (@G gc) (fun a : @G gc => @valid gc a) c v1)) f) (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) a v)) f (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ge (@exist (@G ge) (fun a : @G ge => @valid ge a) e v3)))) *)
      repeat (apply realize_eq in J1; destruct J1 as [? J1]).
(* Goal: @sigT (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (fun f : @sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) => and (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) gb (@exist (@G gb) (fun a : @G gb => @valid gb a) b v0)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) gc (@exist (@G gc) (fun a : @G gc => @valid gc a) c v1)) f) (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) a v)) f (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ge (@exist (@G ge) (fun a : @G ge => @valid ge a) e v3)))) *)
      repeat (apply realize_eq in J2; destruct J2 as [? J2]); subst.
(* Goal: @sigT (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (fun f : @sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) => and (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) b v0)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) c v1)) f) (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) a v)) f (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) e v3)))) *)
      destruct (join_assoc J1 J2) as (f & ? & J).
(* Goal: @sigT (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (fun f : @sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) => and (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) b v0)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) c v1)) f) (@join (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) a v)) f (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) ga (@exist (@G ga) (fun a : @G ga => @valid ga a) e v3)))) *)
      exists (existT _ ga (exist _ f (join_valid _ _ _ (join_comm J) v3))).
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      split; constructor; auto.
    - inversion 1; constructor; auto.
    - inversion 1; subst; inversion 1; subst; auto.
(* Goal: @eq (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) a0 va)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) c vc)) *)
      inv H.
      repeat (match goal with H : existT _ _ _ = existT _ _ _ |- _ => apply inj_pair2 in H end;
          subst).
(* Goal: @eq (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) a0 va)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) c vc)) *)
      f_equal; eapply exist_ext, join_positivity; eauto.
  Qed.

  Instance Perm_ghost : Perm_alg ghost.
  Proof.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
    constructor.
    - intros until 1; revert z'; induction H; inversion 1; subst; auto.
(* Goal: @eq (SM.ghost (@pred rmap ag_rmap)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap)))) a g1) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap)))) o g2) *)
      f_equal; auto.
(* Goal: @eq (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a3 a5 *)
      eapply join_eq; eauto.
    - induction a; intros ???? J1 J2; apply ghost_join_inv in J1; subst.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
      { exists e; split; auto; constructor. }
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join b c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
      destruct b; subst; [eexists; split; eauto; constructor|].
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
      destruct d; [contradiction|].
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
      destruct J1 as [Jc1 J1].
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
      apply ghost_join_inv in J2.
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
      destruct c; subst; [eexists; split; eauto; constructor; auto|].
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o1 c) f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
      destruct e; [contradiction|].
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o1 c) f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o2 e))) *)
      destruct J2 as [Jc2 J2].
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o1 c) f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o2 e))) *)
      destruct (join_assoc Jc1 Jc2) as (f & ? & ?).
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o b) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o1 c) f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) o2 e))) *)
      destruct (IHa _ _ _ _ J1 J2) as (f' & ? & ?).
(* Goal: and (@join resource Join_resource (NO rb n1) (YES rc sc ke pe) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe)) (@join resource Join_resource (NO ra n0) (YES rf (@join_readable2 rb rc rf H3 sc) ke pe) (YES re se ke pe)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
(* Goal: @sigT resource (fun f : resource => and (@join resource Join_resource b c f) (@join resource Join_resource a f e)) *)
      exists (f :: f'); split; constructor; auto.
    - induction 1; constructor; auto.
    - intros until 1; revert b'; induction H; inversion 1; subst; auto.
(* Goal: @eq ghost (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a1 m1) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a3 m3) *)
      f_equal; eauto.
(* Goal: @eq (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a1 a3 *)
      eapply join_positivity; eauto.
  Qed.

  Instance Sep_ghost : Sep_alg ghost.
  Proof.
(* Goal: @Sep_alg ghost ghost_join *)
    intros; exists (fun _ => nil); auto; constructor.
  Defined.

  Lemma ghost_core : forall (g: ghost), core g = nil.
  Proof.
(* Goal: @eq nat n n *)
    auto.
  Qed.

  Definition rmap' := ((address->resource) * ghost)%type.
  Definition preds_fmap (f g:(pred rmap)->(pred rmap)) (x:preds) : preds :=
    match x with SomeP A ls => SomeP A (fmap (fpi _) f g ls) end.

  Lemma preds_fmap_id : preds_fmap (id (pred rmap)) (id (pred rmap)) = id preds.
  Proof.
(* Goal: @eq nat n n *)
    intros; apply extensionality; intro x; destruct x; simpl; auto.
(* Goal: @eq preds (SomeP A (fun i : list Type => @fmap (dependent_type_functor_rec i A) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (id (@pred rmap ag_rmap)) (id (@pred rmap ag_rmap)) (_f i))) (id preds (SomeP A _f)) *)
    unfold id at 3.
(* Goal: @eq (option rmap) (@Some rmap (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap))) n _f))) (@Some K.knot (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n _f))) *)
    f_equal.
(* Goal: @eq (forall i : list Type, _functor (dependent_type_functor_rec i A) (@pred rmap ag_rmap)) (fun i : list Type => @fmap (dependent_type_functor_rec i A) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 g2 (@fmap (dependent_type_functor_rec i A) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f1 f2 (_f i))) (fun i : list Type => @fmap (dependent_type_functor_rec i A) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 f1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f2 g2) (_f i)) *)
    extensionality i.
(* Goal: @eq (_functor (dependent_type_functor_rec i A) (@pred rmap ag_rmap)) (@fmap (dependent_type_functor_rec i A) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (id (@pred rmap ag_rmap)) (id (@pred rmap ag_rmap)) (_f i)) (_f i) *)
    rewrite fmap_id; auto.
  Qed.

  Lemma preds_fmap_comp : forall f1 f2 g1 g2,
    preds_fmap g1 g2 oo preds_fmap f1 f2 = preds_fmap (g1 oo f1) (f2 oo g2).
  Proof.
(* Goal: forall f1 f2 g1 g2 : forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap, @eq (forall _ : preds, preds) (@compose preds preds preds (preds_fmap g1 g2) (preds_fmap f1 f2)) (preds_fmap (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 f1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f2 g2)) *)
    intros; apply extensionality; intro x; destruct x; simpl.
(* Goal: @eq preds (@compose preds preds preds (preds_fmap g1 g2) (preds_fmap f1 f2) (SomeP A _f)) (SomeP A (fun i : list Type => @fmap (dependent_type_functor_rec i A) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 f1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f2 g2) (_f i))) *)
    unfold preds_fmap, compose at 1; simpl.
(* Goal: @eq (option rmap) (@Some rmap (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap))) n _f))) (@Some K.knot (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n _f))) *)
    f_equal.
(* Goal: @eq (forall i : list Type, _functor (dependent_type_functor_rec i A) (@pred rmap ag_rmap)) (fun i : list Type => @fmap (dependent_type_functor_rec i A) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 g2 (@fmap (dependent_type_functor_rec i A) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f1 f2 (_f i))) (fun i : list Type => @fmap (dependent_type_functor_rec i A) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 f1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f2 g2) (_f i)) *)
    extensionality i.
    rewrite <- fmap_comp; auto.
  Qed.

  Definition resource_fmap (f g:pred rmap -> pred rmap) (x:resource) : resource :=
    match x with
    | NO sh nsh => NO sh nsh
    | YES sh rsh k p => YES sh rsh k (preds_fmap f g p)
    | PURE k p => PURE k (preds_fmap f g p)
    end.

  Definition ghost_fmap (f g:pred rmap -> pred rmap)(x:ghost) : ghost :=
    map (option_map (fun '(a, b) => (a, preds_fmap f g b))) x.

  Lemma resource_fmap_id :
    resource_fmap (id (pred rmap)) (id (pred rmap)) = id resource.
  Proof.
(* Goal: @eq (forall _ : rmap', rmap') (rmap_fmap (id (@pred rmap ag_rmap)) (id (@pred rmap ag_rmap))) (id rmap') *)
    intros; apply extensionality; intro x.
(* Goal: @eq resource (resource_fmap (id (@pred rmap ag_rmap)) (id (@pred rmap ag_rmap)) x) (id resource x) *)
    unfold resource_fmap.
(* Goal: @eq nat n n *)
    destruct x; simpl; auto.
(* Goal: @eq nat n n *)
    rewrite preds_fmap_id; auto.
(* Goal: @eq nat n n *)
    rewrite preds_fmap_id; auto.
  Qed.

  Lemma ghost_fmap_id : ghost_fmap (id (pred rmap)) (id (pred rmap)) = id ghost.
  Proof.
(* Goal: forall x : ghost, @eq ghost (g2ghost (ghost2g x)) x *)
    extensionality x; induction x; auto; simpl.
(* Goal: @eq ghost (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@option_map (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (fun '(pair a b) => @pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds a (preds_fmap (id (@pred rmap ag_rmap)) (id (@pred rmap ag_rmap)) b)) a) (ghost_fmap (id (@pred rmap ag_rmap)) (id (@pred rmap ag_rmap)) x)) (id ghost (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a x)) *)
    rewrite IHx; destruct a as [[]|]; auto; simpl.
(* Goal: @eq nat n n *)
    rewrite preds_fmap_id; auto.
  Qed.

  Lemma resource_fmap_comp : forall f1 f2 g1 g2,
    resource_fmap g1 g2 oo resource_fmap f1 f2 = resource_fmap (g1 oo f1) (f2 oo g2).
  Proof.
(* Goal: forall f1 f2 g1 g2 : forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap, @eq (forall _ : rmap', rmap') (@compose rmap' rmap' rmap' (rmap_fmap g1 g2) (rmap_fmap f1 f2)) (rmap_fmap (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 f1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f2 g2)) *)
    intros f1 f2 g1 g2.
(* Goal: @eq nat n n *)
    apply extensionality; intro x; destruct x; simpl; auto.
(* Goal: @eq resource (@compose resource resource resource (resource_fmap g1 g2) (resource_fmap f1 f2) (YES sh r k p)) (YES sh r k (preds_fmap (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 f1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f2 g2) p)) *)
(* Goal: @eq resource (@compose resource resource resource (resource_fmap g1 g2) (resource_fmap f1 f2) (PURE k p)) (PURE k (preds_fmap (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 f1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f2 g2) p)) *)
    unfold compose at 1; simpl.
    rewrite <- preds_fmap_comp; auto.
    rewrite <- preds_fmap_comp; auto.
  Qed.

  Lemma ghost_fmap_comp : forall f1 f2 g1 g2,
    ghost_fmap g1 g2 oo ghost_fmap f1 f2 = ghost_fmap (g1 oo f1) (f2 oo g2).
  Proof.
(* Goal: forall x : ghost, @eq ghost (g2ghost (ghost2g x)) x *)
    intros; extensionality x; induction x; auto; simpl.
    rewrite <- IHx; destruct a as [[]|]; auto; simpl.
    rewrite <- preds_fmap_comp; auto.
  Qed.

  Definition rmap_fmap (f g:(pred rmap)->(pred rmap)) (x:rmap') : rmap' :=
              (resource_fmap f g oo fst x, ghost_fmap f g (snd x)).

  Lemma rmap_fmap_id : rmap_fmap (id (pred rmap)) (id (pred rmap)) = id rmap'.
  Proof.
(* Goal: @eq (forall _ : rmap', rmap') (rmap_fmap (id (@pred rmap ag_rmap)) (id (@pred rmap ag_rmap))) (id rmap') *)
    intros; apply extensionality; intro x.
(* Goal: @eq rmap' (rmap_fmap (id (@pred rmap ag_rmap)) (id (@pred rmap ag_rmap)) x) (id rmap' x) *)
    unfold rmap_fmap; destruct x.
(* Goal: @eq rmap' (@pair (forall _ : address, resource) ghost (fun l : address => res2resource (@fst (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x))) l)) (g2ghost (@snd (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x)))))) x *)
    simpl.
(* Goal: @eq rmap' (@pair (forall _ : address, resource) ghost (@compose address resource resource (resource_fmap (id (@pred rmap ag_rmap)) (id (@pred rmap ag_rmap))) r) (ghost_fmap (id (@pred rmap ag_rmap)) (id (@pred rmap ag_rmap)) g)) (id rmap' (@pair (forall _ : address, resource) ghost r g)) *)
    rewrite resource_fmap_id, ghost_fmap_id.
(* Goal: @eq rmap' (@pair (forall _ : address, resource) ghost (@compose address resource resource (id resource) r) (id ghost g)) (id rmap' (@pair (forall _ : address, resource) ghost r g)) *)
    rewrite (id_unit2 _ (resource) r).
(* Goal: @eq (SM.ghost (@pred rmap ag_rmap)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap)))) a g1) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap)))) o g2) *)
    f_equal; auto.
  Qed.

  Lemma rmap_fmap_comp : forall f1 f2 g1 g2,
    rmap_fmap g1 g2 oo rmap_fmap f1 f2 = rmap_fmap (g1 oo f1) (f2 oo g2).
  Proof.
(* Goal: forall f1 f2 g1 g2 : forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap, @eq (forall _ : rmap', rmap') (@compose rmap' rmap' rmap' (rmap_fmap g1 g2) (rmap_fmap f1 f2)) (rmap_fmap (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 f1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f2 g2)) *)
    intros f1 f2 g1 g2.
(* Goal: @eq (forall _ : rmap', rmap') (@compose rmap' rmap' rmap' (rmap_fmap g1 g2) (rmap_fmap f1 f2)) (rmap_fmap (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 f1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f2 g2)) *)
    unfold rmap_fmap.
(* Goal: @eq (forall _ : rmap', rmap') (@compose rmap' rmap' rmap' (fun x : rmap' => @pair (forall _ : address, resource) ghost (@compose address resource resource (resource_fmap g1 g2) (@fst (forall _ : address, resource) ghost x)) (ghost_fmap g1 g2 (@snd (forall _ : address, resource) ghost x))) (fun x : rmap' => @pair (forall _ : address, resource) ghost (@compose address resource resource (resource_fmap f1 f2) (@fst (forall _ : address, resource) ghost x)) (ghost_fmap f1 f2 (@snd (forall _ : address, resource) ghost x)))) (fun x : rmap' => @pair (forall _ : address, resource) ghost (@compose address resource resource (resource_fmap (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 f1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f2 g2)) (@fst (forall _ : address, resource) ghost x)) (ghost_fmap (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 f1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f2 g2) (@snd (forall _ : address, resource) ghost x))) *)
    apply extensionality; intro x.
(* Goal: @eq rmap' (@compose rmap' rmap' rmap' (fun x : rmap' => @pair (forall _ : address, resource) ghost (@compose address resource resource (resource_fmap g1 g2) (@fst (forall _ : address, resource) ghost x)) (ghost_fmap g1 g2 (@snd (forall _ : address, resource) ghost x))) (fun x : rmap' => @pair (forall _ : address, resource) ghost (@compose address resource resource (resource_fmap f1 f2) (@fst (forall _ : address, resource) ghost x)) (ghost_fmap f1 f2 (@snd (forall _ : address, resource) ghost x))) x) (@pair (forall _ : address, resource) ghost (@compose address resource resource (resource_fmap (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 f1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f2 g2)) (@fst (forall _ : address, resource) ghost x)) (ghost_fmap (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 f1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f2 g2) (@snd (forall _ : address, resource) ghost x))) *)
    unfold compose at 1.
(* Goal: @eq rmap' (@pair (forall _ : address, resource) ghost (fun l : address => res2resource (@fst (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x))) l)) (g2ghost (@snd (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x)))))) x *)
    destruct x as (r,g). simpl.
    rewrite <- compose_assoc.
(* Goal: @eq nat n n *)
    rewrite resource_fmap_comp; auto.
(* Goal: @eq (SM.ghost (@pred rmap ag_rmap)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap)))) a g1) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap)))) o g2) *)
    f_equal; auto.
(* Goal: @eq ghost (ghost_fmap g1 g2 (ghost_fmap f1 f2 g)) (ghost_fmap (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 f1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f2 g2) g) *)
    pose proof ghost_fmap_comp as HG.
    unfold compose in HG at 1; rewrite <- HG.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
    intros.
(* Goal: @eq nat n n *)
    f_equal; proof_irr; auto.
  Qed.

  Definition rmap'2pre_rmap (f: rmap') : f_pre_rmap (pred rmap) :=
      (fun x : address => resource2res (fst f x), ghost2g (snd f)).

  Definition pre_rmap2rmap' (f: f_pre_rmap (pred rmap)) : rmap' :=
      (fun l : address => res2resource (fst f l), g2ghost (snd f)).

  Lemma rmap'2pre_rmap2rmap' :
    forall x, rmap'2pre_rmap (pre_rmap2rmap' x) = x.
  Proof.
(* Goal: forall x : rmap', @eq rmap' (pre_rmap2rmap' (rmap'2pre_rmap x)) x *)
    intro. unfold rmap'2pre_rmap, pre_rmap2rmap'. simpl.
(* Goal: @eq (option rmap) (@Some rmap (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap))) n _f))) (@Some K.knot (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n _f))) *)
    destruct x; simpl; f_equal.
(* Goal: @eq nat n n *)
    extensionality x; rewrite res2resource2res; auto.
(* Goal: @eq nat n n *)
    rewrite g2ghost2g; auto.
  Qed.

  Lemma pre_rmap2rmap'2pre_rmap :
    forall x,  pre_rmap2rmap' (rmap'2pre_rmap x) = x.
  Proof.
(* Goal: forall x : rmap', @eq rmap' (pre_rmap2rmap' (rmap'2pre_rmap x)) x *)
    intro.
(* Goal: @eq rmap' (@pair (forall _ : address, resource) ghost (fun l : address => res2resource (@fst (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x))) l)) (g2ghost (@snd (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x)))))) x *)
    unfold rmap'2pre_rmap, pre_rmap2rmap'. simpl.
(* Goal: @eq (option rmap) (@Some rmap (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap))) n _f))) (@Some K.knot (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n _f))) *)
    destruct x; simpl; f_equal.
(* Goal: @eq nat n n *)
    extensionality x; rewrite resource2res2resource; auto.
(* Goal: @eq nat n n *)
    rewrite ghost2g2ghost; auto.
  Qed.

  Definition squash (n_rm:nat * rmap') : rmap :=
    match n_rm with (n,rm) => K.squash (n, rmap'2pre_rmap rm) end.

  Definition unsquash (phi:rmap) : (nat * rmap') :=
    match K.unsquash phi with (n,rm) => (n, pre_rmap2rmap' rm) end.

  Definition rmap_level (phi:rmap) : nat := fst (unsquash phi).
  Definition resource_at (phi:rmap) : address -> resource := fst (snd (unsquash phi)).
  Infix "@" := resource_at (at level 50, no associativity).
  Definition ghost_of (phi:rmap) : ghost := snd (snd (unsquash phi)).

(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join b c f) (@join ghost ghost_join (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) f e)) *)
(* Goal: @sigT ghost (fun f : ghost => and (@join ghost ghost_join b c f) (@join ghost ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a a0) f e)) *)
  Lemma pred_ext': forall {A} `{agA: ageable A} P Q,
                (forall x, app_pred P x <-> app_pred Q x) -> P = Q.
  Proof. intros; apply pred_ext; intro; apply H; auto. Qed.

  Lemma squash_unsquash : forall phi, squash (unsquash phi) = phi.
  Proof.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
    intros.
(* Goal: @eq rmap' (@pair (forall _ : address, resource) ghost (fun l : address => res2resource (@fst (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x))) l)) (g2ghost (@snd (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x)))))) x *)
    unfold squash, unsquash; simpl.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
    destruct (K.unsquash phi) eqn:?H; simpl; intros.
(* Goal: @eq (option rmap) (@Some rmap (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap))) n (rmap'2pre_rmap (pre_rmap2rmap' _f))))) (@Some K.knot (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n _f))) *)
    rewrite rmap'2pre_rmap2rmap'.
    unfold K.KI.F in *.
(* Goal: @eq rmap (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap))) n _f)) phi *)
    unfold f_pre_rmap in H.
    match goal with
    | |- K.squash ?A = _ => replace A with (K.unsquash phi)
    end.
(* Goal: @eq nat n n *)
    rewrite K.squash_unsquash; auto.
  Qed.

  Program Definition approx (n:nat) (p: (pred rmap)) : (pred rmap) :=
    fun w => level w < n /\ p w.
  Next Obligation.
(* Goal: and (lt (@level rmap ag_rmap a') n) (@app_pred rmap ag_rmap p a') *)
  destruct H0.
(* Goal: and (lt (@level rmap ag_rmap a') n) (@app_pred rmap ag_rmap p a') *)
  split.
(* Goal: lt (@level rmap ag_rmap a') n *)
(* Goal: @app_pred rmap ag_rmap p a' *)
  apply age_level in H.
  simpl in *. omega.
(* Goal: @app_pred rmap ag_rmap p a' *)
  apply pred_hereditary with a; auto.
  Qed.

  Lemma approx_K_approx: approx = K.approx.
  Proof.
(* Goal: @eq (forall (_ : nat) (_ : @pred rmap ag_rmap), @pred rmap ag_rmap) approx K.approx *)
    extensionality n p.
(* Goal: @eq (@pred rmap ag_rmap) (approx n p) (K.approx n p) *)
    apply pred_ext'; intros w.
(* Goal: @eq rmap' (@pair (forall _ : address, resource) ghost (fun l : address => res2resource (@fst (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x))) l)) (g2ghost (@snd (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x)))))) x *)
    unfold approx, compose; simpl.
(* Goal: iff (and (lt (@level rmap ag_rmap w) n) (@app_pred rmap ag_rmap p w)) (@app_pred rmap ag_rmap (K.approx n p) w) *)
    rewrite K.approx_spec.
    unfold rmap_level, unsquash; simpl;
    repeat rewrite K.knot_level;
    repeat rewrite setset, setget;     intuition.
  Qed.

  Lemma unsquash_squash : forall n rm, (unsquash (squash (n,rm))) = (n,rmap_fmap (approx n) (approx n) rm).
  Proof.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
    intros.
(* Goal: @eq (option rmap) (let (n0, x) := unsquash x in match n0 with | O => @None rmap | S n => @Some rmap (squash (@pair nat rmap' n x)) end) (let (n0, x) := K.unsquash x in match n0 with | O => @None K.knot | S n => @Some K.knot (K.squash (@pair nat (_functor K.KI.F (@pred K.knot K.ageable_knot)) n x)) end) *)
    unfold unsquash, squash.
    rewrite K.unsquash_squash. unfold K.KI.F, f_pre_rmap.
    match goal with [|- (_,?X) = (_,?Y) ] =>
      replace Y with X; auto
    end.
    match goal with [|- pre_rmap2rmap' ?X = _ ] =>
      replace X with
        (fmap f_pre_rmap (K.approx n) (K.approx n) (rmap'2pre_rmap rm))
    end.
    2: repeat rewrite <- fmap_comp.
(* Goal: @eq nat n n *)
    2: unfold compose; auto.
(* Goal: @eq (option rmap) (@Some rmap (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap))) n _f))) (@Some K.knot (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n _f))) *)
    destruct rm; simpl. unfold pre_rmap2rmap', rmap_fmap. simpl; f_equal.
    extensionality l.
(* Goal: @join resource Join_resource (res2resource (@fst (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) f l)) (res2resource (@fst (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) f0 l)) (res2resource (@fst (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) f1 l)) *)
(* Goal: @join ghost ghost_join (@snd (forall _ : address, resource) ghost (pre_rmap2rmap' f)) (@snd (forall _ : address, resource) ghost (pre_rmap2rmap' f0)) (@snd (forall _ : address, resource) ghost (pre_rmap2rmap' f1)) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
    unfold compose.
(* Goal: @eq nat n n *)
    destruct (r l); simpl; auto.
    (* YES *)
(* Goal: @eq rmap' (@pair (forall _ : address, resource) ghost (fun l : address => res2resource (@fst (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x))) l)) (g2ghost (@snd (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x)))))) x *)
    destruct p; simpl.
(* Goal: @eq nat n n *)
    rewrite approx_K_approx; auto.
    (* PURE *)
(* Goal: @eq rmap' (@pair (forall _ : address, resource) ghost (fun l : address => res2resource (@fst (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x))) l)) (g2ghost (@snd (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x)))))) x *)
    destruct p; simpl.
(* Goal: @eq nat n n *)
    rewrite approx_K_approx; auto.
    (* ghost *)
(* Goal: @eq rmap' (@pair (forall _ : address, resource) ghost (fun l : address => res2resource (@fst (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x))) l)) (g2ghost (@snd (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x)))))) x *)
    induction g; auto; simpl.
(* Goal: @eq rmap' (@pair (forall _ : address, resource) ghost (fun l : address => res2resource (@fst (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x))) l)) (g2ghost (@snd (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x)))))) x *)
    setoid_rewrite IHg; destruct a as [[]|]; auto; simpl.
(* Goal: @eq (option rmap) (@Some rmap (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap))) n _f))) (@Some K.knot (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n _f))) *)
    repeat f_equal.
(* Goal: @eq ghost (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds s (p2pred (pred2p p)))) x) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds s p)) x) *)
    rewrite approx_K_approx; destruct p; auto.
  Qed.

  Instance Join_nat_rmap': Join (nat * rmap') := Join_prod _ (Join_equiv nat) _ _.
(*
Lemma fmap_p2p'_inj:
  forall p q,
        fmap SM.preds K.predicate K.predicate (@pred rmap ag_rmap) p =
        fmap SM.preds K.predicate K.predicate (@pred rmap ag_rmap) q ->
        p=q.
Proof.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
  intros.
  destruct p as [p Vp]. destruct q as [q Vq].
  unfold fmap in *. unfold f_preds in *. simpl in *.
(* Goal: @eq (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) a0 va)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) c vc)) *)
  inv H.
(* Goal: @eq (option rmap) (@Some rmap (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap))) n _f))) (@Some K.knot (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n _f))) *)
  f_equal.
  apply inj_pair2 in H2. unfold ffun_fmap, f_identity in *.
  unfold fmap, compose in H2.
  extensionality w.
 apply equal_f with w in H2. unfold fidentity_fmap in *.
  unfold p2p' in *. inv H2.
  unfold K.predicate in *.
  apply pred_ext'. intros [k o]. destruct o.
  apply equal_f with k in H0. rewrite H0; intuition.
Qed.
*)
  Lemma g2ghost_inv: forall g1 g2, g2ghost g1 = g2ghost g2 -> g1 = g2.
  Proof.
(* Goal: @eq nat n n *)
    induction g1; destruct g2; inversion 1; auto.
(* Goal: @eq (SM.ghost (@pred rmap ag_rmap)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap)))) a g1) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap)))) o g2) *)
    f_equal; auto.
(* Goal: @eq nat n n *)
    destruct a as [[]|], o as [[]|]; inv H1; auto.
(* Goal: @eq nat n n *)
    destruct _f, _f0; inv H4; auto.
  Qed.

  Lemma join_unsquash : forall phi1 phi2 phi3,
    join phi1 phi2 phi3 <->
    join (unsquash phi1) (unsquash phi2) (unsquash phi3).
  Proof.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
    intros.
(* Goal: @eq nat ((let (level, age1, _) := K.ageable_knot in level) x) (@fst nat rmap' (unsquash x)) *)
    unfold unsquash.
(* Goal: iff (@join rmap Join_rmap phi1 phi2 phi3) (@join (prod nat rmap') Join_nat_rmap' (let (n, rm) := K.unsquash phi1 in @pair nat rmap' n (pre_rmap2rmap' rm)) (let (n, rm) := K.unsquash phi2 in @pair nat rmap' n (pre_rmap2rmap' rm)) (let (n, rm) := K.unsquash phi3 in @pair nat rmap' n (pre_rmap2rmap' rm))) *)
    rewrite KSa.join_unsquash.
(* Goal: iff (@join (prod nat (_functor KSa.K.KI.F KSa.K.predicate)) KSa.Join_nat_F (KSa.K.unsquash phi1) (KSa.K.unsquash phi2) (KSa.K.unsquash phi3)) (@join (prod nat rmap') Join_nat_rmap' (let (n, rm) := K.unsquash phi1 in @pair nat rmap' n (pre_rmap2rmap' rm)) (let (n, rm) := K.unsquash phi2 in @pair nat rmap' n (pre_rmap2rmap' rm)) (let (n, rm) := K.unsquash phi3 in @pair nat rmap' n (pre_rmap2rmap' rm))) *)
    destruct (K.unsquash phi1) as [n f].
(* Goal: iff (@join (prod nat (_functor KSa.K.KI.F KSa.K.predicate)) KSa.Join_nat_F (@pair nat (_functor K.KI.F (@pred K.knot K.ageable_knot)) n f) (KSa.K.unsquash phi2) (KSa.K.unsquash phi3)) (@join (prod nat rmap') Join_nat_rmap' (@pair nat rmap' n (pre_rmap2rmap' f)) (let (n, rm) := K.unsquash phi2 in @pair nat rmap' n (pre_rmap2rmap' rm)) (let (n, rm) := K.unsquash phi3 in @pair nat rmap' n (pre_rmap2rmap' rm))) *)
    destruct (K.unsquash phi2) as [n0 f0].
(* Goal: iff (@join (prod nat (_functor KSa.K.KI.F KSa.K.predicate)) KSa.Join_nat_F (@pair nat (_functor K.KI.F (@pred K.knot K.ageable_knot)) n f) (@pair nat (_functor K.KI.F (@pred K.knot K.ageable_knot)) n0 f0) (KSa.K.unsquash phi3)) (@join (prod nat rmap') Join_nat_rmap' (@pair nat rmap' n (pre_rmap2rmap' f)) (@pair nat rmap' n0 (pre_rmap2rmap' f0)) (let (n, rm) := K.unsquash phi3 in @pair nat rmap' n (pre_rmap2rmap' rm))) *)
    destruct (K.unsquash phi3) as [n1 f1].
(* Goal: iff (@join (prod nat (_functor KSa.K.KI.F KSa.K.predicate)) KSa.Join_nat_F (@pair nat (_functor K.KI.F (@pred K.knot K.ageable_knot)) n f) (@pair nat (_functor K.KI.F (@pred K.knot K.ageable_knot)) n0 f0) (@pair nat (_functor K.KI.F (@pred K.knot K.ageable_knot)) n1 f1)) (@join (prod nat rmap') Join_nat_rmap' (@pair nat rmap' n (pre_rmap2rmap' f)) (@pair nat rmap' n0 (pre_rmap2rmap' f0)) (@pair nat rmap' n1 (pre_rmap2rmap' f1))) *)
    simpl; intuition.
    destruct H; simpl in *; split; simpl; auto.
(* Goal: @join (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate)) (KSa.KSAI.Join_F KSa.K.predicate) f f0 f1 *)
    inversion H0.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
    constructor.
(* Goal: @join (forall _ : AV.address, res KSa.K.predicate) (Join_fun AV.address (res KSa.K.predicate) (SM.res_join KSa.K.predicate)) (@fst (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f) (@fst (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f0) (@fst (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f1) *)
(* Goal: @join (SM.ghost KSa.K.predicate) (SM.ghost_join KSa.K.predicate) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f0) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f1) *)
    intro l; specialize ( H1 l).
    simpl in *.
(* Goal: @join resource Join_resource (res2resource (@fst (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) f l)) (res2resource (@fst (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) f0 l)) (res2resource (@fst (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) f1 l)) *)
(* Goal: @join ghost ghost_join (@snd (forall _ : address, resource) ghost (pre_rmap2rmap' f)) (@snd (forall _ : address, resource) ghost (pre_rmap2rmap' f0)) (@snd (forall _ : address, resource) ghost (pre_rmap2rmap' f1)) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
    unfold compose.
    destruct f, f0, f1; simpl in *.
(* Goal: @eq rmap' (@pair (forall _ : address, resource) ghost (fun l : address => res2resource (@fst (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x))) l)) (g2ghost (@snd (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x)))))) x *)
    inv H1; simpl.
(* Goal: @eq nat n n *)
    constructor; auto.
    destruct p. simpl in *. constructor; auto. destruct p. simpl in *. constructor; auto.
    destruct p; simpl in *.
(* Goal: @eq nat n n *)
    constructor; auto.
    destruct p; simpl in *.
(* Goal: @eq nat n n *)
    constructor; auto.

    destruct f, f0, f1; simpl in *. 
    clear - H2; induction H2; constructor; auto.
(* Goal: @join (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Join_lower (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join preds preds_join)) (@option_map (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap))) (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (fun '(pair a b) => @pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds a (p2pred b)) a1) (@option_map (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap))) (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (fun '(pair a b) => @pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds a (p2pred b)) a2) (@option_map (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred rmap ag_rmap))) (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (fun '(pair a b) => @pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds a (p2pred b)) a3) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
    inv H; constructor; auto.
    destruct a0, a4, a5; inv H0; simpl in *.
(* Goal: @eq nat n n *)
    inv H; inv H1; constructor; constructor; auto.

    destruct H; simpl in *; split; simpl; auto.
(* Goal: @join (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate)) (KSa.KSAI.Join_F KSa.K.predicate) f f0 f1 *)
    inversion H0.
(* Goal: @join (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate)) (KSa.KSAI.Join_F KSa.K.predicate) f f0 f1 *)
    hnf in H1. simpl proj1_sig in H1.
(* Goal: @eq nat n n *)
    constructor; auto.
(* Goal: @join (forall _ : AV.address, res KSa.K.predicate) (Join_fun AV.address (res KSa.K.predicate) (SM.res_join KSa.K.predicate)) (@fst (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f) (@fst (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f0) (@fst (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f1) *)
(* Goal: @join (SM.ghost KSa.K.predicate) (SM.ghost_join KSa.K.predicate) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f0) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f1) *)
    intro l; specialize ( H1 l).
(* Goal: @join (res KSa.K.predicate) (SM.res_join KSa.K.predicate) (@fst (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f l) (@fst (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f0 l) (@fst (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f1 l) *)
(* Goal: @join (SM.ghost KSa.K.predicate) (SM.ghost_join KSa.K.predicate) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f0) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f1) *)
    simpl proj1_sig.
    clear - H1.
    destruct f, f0, f1; simpl in *.
(* Goal: @join (res KSa.K.predicate) (SM.res_join KSa.K.predicate) (r l) (r0 l) (r1 l) *)
(* Goal: @join (SM.ghost KSa.K.predicate) (SM.ghost_join KSa.K.predicate) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f0) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f1) *)
    forget (r l) as a; forget (r0 l) as b; forget (r1 l) as c.
    clear - H1.
    unfold res2resource in *. unfold res_fmap in *.
    destruct a as [ra | ra sha ka pa| ka pa]; try destruct pa as [? ?p];
    destruct b as [rb | rb shb kb pb|kb pb]; try destruct pb as [? ?p];
    destruct c as [rc | rc shc kc pc|kc pc]; try destruct pc as [? ?p];
    inv H1.
    + constructor; auto.
    + apply inj_pair2 in H8. subst p0. constructor; auto.
    + apply inj_pair2 in H8. subst p0. constructor; auto.
    + subst. apply inj_pair2 in H11. subst p1. apply inj_pair2 in H7; subst p0.
(* Goal: @eq nat n n *)
      constructor; auto.
    + subst ; apply inj_pair2 in H8. subst p1. apply inj_pair2 in H5. subst p0.
(* Goal: @eq nat n n *)
      constructor; auto.
    + simpl in *.
      destruct f, f0, f1; simpl in *.
      clear - H2.
(* Goal: @join (SM.ghost KSa.K.predicate) (SM.ghost_join KSa.K.predicate) g g0 g1 *)
      remember (g2ghost g) as a; remember (g2ghost g0) as b; remember (g2ghost g1) as c.
(* Goal: @join (res KSa.K.predicate) (SM.res_join KSa.K.predicate) (YES' (@pred K.knot K.ageable_knot) ra sha kc (@existT TypeTree (fun i : TypeTree => _functor (@fpi (list Type) (fun ts : list Type => dependent_type_functor_rec ts i)) (@pred K.knot K.ageable_knot)) x1 p)) (YES' (@pred K.knot K.ageable_knot) rb shb kc (@existT TypeTree (fun i : TypeTree => _functor (@fpi (list Type) (fun ts : list Type => dependent_type_functor_rec ts i)) (@pred K.knot K.ageable_knot)) x1 p)) (YES' (@pred K.knot K.ageable_knot) rc shc kc (@existT TypeTree (fun i : TypeTree => _functor (@fpi (list Type) (fun ts : list Type => dependent_type_functor_rec ts i)) (@pred K.knot K.ageable_knot)) x1 p)) *)
      revert dependent g1; revert dependent g0; revert dependent g; induction H2; intros; subst.
      * apply g2ghost_inv in Heqc; subst; destruct g; [constructor | discriminate].
      * apply g2ghost_inv in Heqc; subst; destruct g0; [constructor | discriminate].
      * destruct g, g0, g1; inv Heqa; inv Heqb; inv Heqc.
(* Goal: @join (SM.ghost KSa.K.predicate) (SM.ghost_join KSa.K.predicate) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred K.knot K.ageable_knot)))) o g) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred K.knot K.ageable_knot)))) o0 g0) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds (@pred K.knot K.ageable_knot)))) o1 g1) *)
        constructor; [|apply IHghost_join; auto].
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
        destruct o as [[]|], o0 as [[]|], o1 as [[]|]; inv H; try constructor.
        -- destruct _f, _f0, _f1; inv H4; simpl in *.
(* Goal: @join (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot)))) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) SM.ghost_elem_join (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot))) (SM.preds_join (@pred K.knot K.ageable_knot))) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot))) s (@existT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot)) x _f)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot))) s0 (@existT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot)) x0 _f0)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot))) s1 (@existT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot)) x1 _f1)) *)
           inv H; inv H0.
(* Goal: @join (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot)))) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) SM.ghost_elem_join (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot))) (SM.preds_join (@pred K.knot K.ageable_knot))) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot))) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g2 (@exist (@G g2) (fun a : @G g2 => @valid g2 a) a va)) (@existT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot)) x _f)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot))) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g2 (@exist (@G g2) (fun a : @G g2 => @valid g2 a) b vb)) (@existT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot)) x0 _f0)) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@sigT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot))) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g2 (@exist (@G g2) (fun a : @G g2 => @valid g2 a) c vc)) (@existT TypeTree (fun i : TypeTree => forall i0 : list Type, _functor (dependent_type_functor_rec i0 i) (@pred K.knot K.ageable_knot)) x1 _f1)) *)
           inv H; inv H3.
           repeat (match goal with H : existT _ _ _ = existT _ _ _ |- _ => apply inj_pair2 in H end;
(* Goal: @eq nat n n *)
             subst); constructor; constructor; auto.
        -- destruct _f, _f0; inv H4.
           repeat (match goal with H : existT _ _ _ = existT _ _ _ |- _ => apply inj_pair2 in H end;
(* Goal: @eq nat n n *)
             subst); constructor; auto.
        -- destruct _f, _f0; inv H4.
           repeat (match goal with H : existT _ _ _ = existT _ _ _ |- _ => apply inj_pair2 in H end;
(* Goal: @eq nat n n *)
             subst); constructor; auto.
  Qed.

  Lemma ghost_of_core : forall phi, ghost_of (core phi) = core (ghost_of phi).
  Proof.
(* Goal: forall phi : rmap, @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap phi)) (@core ghost ghost_join Sep_ghost (ghost_of phi)) *)
    intro; rewrite KSa.core_unsquash.
(* Goal: @eq ghost (ghost_of (KSa.K.squash (@core (prod nat (_functor KSa.K.KI.F KSa.K.predicate)) KSa.Join_nat_F KSa.Sep_nat_F (KSa.K.unsquash phi)))) (@core ghost ghost_join Sep_ghost (ghost_of phi)) *)
    unfold ghost_of, KSa.K.unsquash, KSa.K.squash, unsquash, squash.
(* Goal: @eq rmap' (@pair (forall _ : address, resource) ghost (fun l : address => res2resource (@fst (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x))) l)) (g2ghost (@snd (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x)))))) x *)
    destruct (K.unsquash phi); simpl.
(* Goal: @eq rmap' (@pair (forall _ : address, resource) ghost (fun l : address => res2resource (@fst (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x))) l)) (g2ghost (@snd (_functor (ffunc (fconst AV.address) f_res) (@pred rmap ag_rmap)) (_functor f_ghost (@pred rmap ag_rmap)) (@pair (forall _ : address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap)) (fun x0 : address => resource2res (@fst (forall _ : address, resource) ghost x x0)) (ghost2g (@snd (forall _ : address, resource) ghost x)))))) x *)
    rewrite K.unsquash_squash; simpl.
(* Goal: @eq nat n n *)
    setoid_rewrite (pre_rmap_core _ _f). auto.
Qed.

  Definition rmap_age1 (k:rmap) : option rmap :=
    match unsquash k with
    | (O,_) => None
    | (S n,x) => Some (squash (n,x))
    end.

  Definition rmap_unage (k:rmap) : rmap :=
    match unsquash k with
    | (n,x) => squash (S n, x)
    end.

  Lemma rmap_age1_knot_age1 :
    rmap_age1 = @age1 _ K.ageable_knot.
  Proof.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
    extensionality x.
(* Goal: @eq (option rmap) (rmap_age1 x) (@age1 K.knot K.ageable_knot x) *)
    unfold rmap_age1.
    rewrite  K.knot_age1.
(* Goal: @eq (option rmap) (let (n0, x) := unsquash x in match n0 with | O => @None rmap | S n => @Some rmap (squash (@pair nat rmap' n x)) end) (let (n0, x) := K.unsquash x in match n0 with | O => @None K.knot | S n => @Some K.knot (K.squash (@pair nat (_functor K.KI.F (@pred K.knot K.ageable_knot)) n x)) end) *)
    unfold unsquash, squash.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
    case (K.unsquash x); simpl; intros.
(* Goal: @eq nat n n *)
    destruct n; auto.
(* Goal: @eq (option rmap) (@Some rmap (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap))) n (rmap'2pre_rmap (pre_rmap2rmap' _f))))) (@Some K.knot (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n _f))) *)
    rewrite rmap'2pre_rmap2rmap'.
(* Goal: @eq (option rmap) (@Some rmap (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred rmap ag_rmap)) (SM.ghost (@pred rmap ag_rmap))) n _f))) (@Some K.knot (K.squash (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n _f))) *)
    f_equal.
  Qed.

  Lemma rmap_age1_eq: @age1 _ ag_rmap = rmap_age1.
  Proof.
(* Goal: @eq nat n n *)
   unfold age1. unfold ag_rmap; simpl; auto.
(* Goal: @eq (_functor f_pre_rmap A) (@core (_functor f_pre_rmap A) (Join_pre_rmap A) (Sep_pre_rmap A) m) (@core (_functor (fpair (ffunc (fconst address) f_res) f_ghost) A) (Join_prod (_functor (ffunc (fconst address) f_res) A) (Join_pi (_functor (fconst address) A) (fun _ : _functor (fconst address) A => _functor f_res A) (fun _ : _functor (fconst address) A => Join_res A)) (_functor f_ghost A) (ghost_join A)) (@Sep_prod (_functor (ffunc (fconst address) f_res) A) (Join_pi (_functor (fconst address) A) (fun _ : _functor (fconst address) A => _functor f_res A) (fun _ : _functor (fconst address) A => Join_res A)) (_functor f_ghost A) (ghost_join A) (Sep_pi (_functor (fconst address) A) (fun _ : _functor (fconst address) A => _functor f_res A) (fun _ : _functor (fconst address) A => Join_res A) (fun _ : _functor (fconst address) A => sa_rj A)) (sa_gj A)) m) *)
   rewrite rmap_age1_knot_age1; reflexivity.
  Qed.

  Lemma rmap_level_eq: @level rmap ag_rmap = fun x => fst (unsquash x).
  Proof.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
    intros.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
   extensionality x.  unfold level.  unfold ag_rmap.
(* Goal: @eq nat ((let (level, age1, _) := K.ageable_knot in level) x) (@fst nat rmap' (unsquash x)) *)
   unfold KSa.K.ageable_knot. unfold unsquash.
(* Goal: @eq nat n n *)
   rewrite K.knot_level. destruct (K.unsquash x); simpl. auto.
  Qed.

(*  Lemma unevolve_identity_rmap :
   (* REMARK:  This may not be needed for anything, so for now it's removed
     from the Module Type *)
    forall w w':rmap, necR w w' -> identity w' -> identity w.
  Proof.
(* Goal: @eq (forall _ : rmap, nat) (@level rmap ag_rmap) (fun x : rmap => @fst nat rmap' (unsquash x)) *)
    intros.
(* Goal: @eq nat n n *)
    induction H; eauto.
    rewrite identity_unit_equiv in H0.
    rewrite identity_unit_equiv.
    red in H0. red.
    rewrite join_unsquash in H0.
    rewrite join_unsquash.
    hnf in H. unfold rmap, ag_rmap in H. rewrite <- rmap_age1_knot_age1 in H.
    unfold rmap_age1 in H.
   destruct (unsquash x).
(* Goal: @eq (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) a0 va)) (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) g (@exist (@G g) (fun a : @G g => @valid g a) c vc)) *)
   destruct n. inv H.
    assert (y = squash (n,r)).
(* Goal: @eq nat n n *)
    inv H; auto.
    subst y.
    rewrite unsquash_squash in H0.
(* Goal: and (lt (@level rmap ag_rmap a') n) (@app_pred rmap ag_rmap p a') *)
    destruct H0.
    destruct H1.
(* Goal: and (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) x)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds B))) (ghost_fmap A B f g x))) (@eq (ghost B) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o0 y')) (ghost_fmap A B f g (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) (_functor fpreds A))) o y))) *)
    split; auto.
(* Goal: and (lt (@level rmap ag_rmap a') n) (@app_pred rmap ag_rmap p a') *)
    split.
(* Goal: @join (forall _ : AV.address, res KSa.K.predicate) (Join_fun AV.address (res KSa.K.predicate) (SM.res_join KSa.K.predicate)) (@fst (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f) (@fst (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f0) (@fst (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f1) *)
(* Goal: @join (SM.ghost KSa.K.predicate) (SM.ghost_join KSa.K.predicate) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f0) (@snd (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate) f1) *)
    intro l; specialize ( H1 l).
    destruct r.
    simpl in *.
    unfold compose in *.
    destruct (fst x0 l); simpl in *.
(* Goal: @eq nat n n *)
    constructor; auto.
(* Goal: @eq nat n n *)
    inv H1; auto.
(* Goal: @eq nat n n *)
    inv H1. constructor; auto.
(* Goal: @join rmap' (Join_prod (forall _ : address, resource) (Join_pi address (fun _ : address => resource) (fun _ : address => Join_resource)) ghost ghost_join) (pre_rmap2rmap' f) (pre_rmap2rmap' f0) (pre_rmap2rmap' f1) *)
(* Goal: @join (prod nat (prod (forall _ : AV.address, res KSa.K.predicate) (SM.ghost KSa.K.predicate))) KSa.Join_nat_F (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n f) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n0 f0) (@pair nat (prod (forall _ : AV.address, res (@pred K.knot K.ageable_knot)) (SM.ghost (@pred K.knot K.ageable_knot))) n1 f1) *)
    constructor.
    simpl in *.
  Qed.*)

End Rmaps.
Local Close Scope nat_scope.

