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

Require Import VST.msl.base.
Local Open Scope nat_scope.

Require Import VST.msl.ageable.
Require Import VST.msl.functors.
Require Import VST.msl.sepalg.
Require Import VST.msl.sepalg_functors.
Require Import VST.msl.sepalg_generators.
Require Import VST.msl.age_sepalg.
Require Import VST.msl.knot_full_variant.

Module Type KNOT_FULL_BASIC_INPUT.
  Parameter F: MixVariantFunctor.functor.
End KNOT_FULL_BASIC_INPUT.

Module Type KNOT_FULL_SA_INPUT.
  Declare Module KI: KNOT_FULL_BASIC_INPUT.
  Import MixVariantFunctor.
  Import KI.

  Parameter Join_F: forall A, Join (F A). Existing Instance Join_F.
  Parameter paf_F : pafunctor F Join_F.
  Parameter Perm_F: forall A, Perm_alg (F A).
  Parameter Sep_F: forall A, Sep_alg (F A).
End KNOT_FULL_SA_INPUT.

Module Type KNOT_BASIC.
  Declare Module KI:KNOT_FULL_BASIC_INPUT.
  Import MixVariantFunctor.
  Import KI.
  Parameter knot: Type.
  Parameter ageable_knot : ageable knot.
  Existing Instance ageable_knot.

  Parameter predicate: Type.
  Parameter squash : (nat * F predicate) -> knot.
  Parameter unsquash : knot -> (nat * F predicate).
  Parameter approx : nat -> predicate -> predicate.

  Axiom squash_unsquash : forall k:knot, squash (unsquash k) = k.

  Axiom unsquash_squash : forall (n:nat) (f:F predicate),
    unsquash (squash (n,f)) = (n, fmap F (approx n) (approx n) f).

  Axiom knot_age1 : forall k:knot,
    age1 k =
    match unsquash k with
    | (O,_) => None
    | (S n,x) => Some (squash (n,x))
    end.

  Axiom knot_level : forall k:knot,
    level k = fst (unsquash k).

End KNOT_BASIC.

Module Type KNOT_BASIC_LEMMAS.

  Declare Module K: KNOT_BASIC.
  Import MixVariantFunctor.
  Import K.KI.
  Import K.

  Axiom unsquash_inj : forall k1 k2,
    unsquash k1 = unsquash k2 ->
    k1 = k2.

  Axiom unsquash_approx : forall k n Fp,
    unsquash k = (n, Fp) ->
    Fp = fmap F (approx n) (approx n) Fp.
  Arguments unsquash_approx [k n Fp] _.

  Axiom approx_approx1 : forall m n,
    approx n = approx n oo approx (m+n).

  Axiom approx_approx2 : forall m n,
    approx n = approx (m+n) oo approx n.

End KNOT_BASIC_LEMMAS.

Module Type KNOT_FULL_SA.
  Declare Module KI: KNOT_FULL_BASIC_INPUT.
  Declare Module KSAI: KNOT_FULL_SA_INPUT with Module KI := KI.
  Declare Module K: KNOT_BASIC with Module KI := KI.
  Declare Module KL: KNOT_BASIC_LEMMAS with Module K := K.

  Import KI.
  Import KSAI.
  Import K.
  Import KL.

  Parameter Join_knot: Join knot.  Existing Instance Join_knot.
  Parameter Perm_knot : Perm_alg knot.  Existing Instance Perm_knot.
  Parameter Sep_knot : Sep_alg knot.  Existing Instance Sep_knot.
  Instance Join_nat_F: Join (nat * F predicate) :=
       Join_prod nat  (Join_equiv nat) (F predicate) _.
  Instance Perm_nat_F : Perm_alg (nat * F predicate) :=
    @Perm_prod nat _ _ _ (Perm_equiv _) (Perm_F _).
  Instance Sep_nat_F : Sep_alg (nat * F predicate) :=
    @Sep_prod nat _ _ _ (Sep_equiv _) (Sep_F predicate).

  Axiom join_unsquash : forall x1 x2 x3 : knot,
    join x1 x2 x3 = join (unsquash x1) (unsquash x2) (unsquash x3).
  Axiom core_unsquash : forall x, core x = squash (core (unsquash x)).

  Axiom asa_knot : Age_alg knot.

End KNOT_FULL_SA.

Module KnotFullSa
  (KSAI': KNOT_FULL_SA_INPUT)
  (K': KNOT_BASIC with Module KI:=KSAI'.KI)
  (KL': KNOT_BASIC_LEMMAS with Module K:=K'):
  KNOT_FULL_SA with Module KI := KSAI'.KI
               with Module KSAI := KSAI'
               with Module K:=K'
               with Module KL := KL'.

  Module KI := KSAI'.KI.
  Module KSAI := KSAI'.
  Module K := K'.
  Module KL := KL'.

  Import MixVariantFunctor.
  Import MixVariantFunctorLemmas.
  Import KI.
  Import KSAI.
  Import K.
  Import KL.

  Instance Join_nat_F: Join (nat * F predicate) :=
       Join_prod nat  (Join_equiv nat) (F predicate) _.
  Instance Perm_nat_F : Perm_alg (nat * F predicate) :=
      @Perm_prod nat _ _ _ (Perm_equiv _) (Perm_F _).
  Instance Sep_nat_F: Sep_alg (nat * F predicate) :=
      @Sep_prod nat _ _ _ (Sep_equiv _) (Sep_F predicate).

  Lemma unsquash_squash_join_hom : join_hom (unsquash oo squash).
  Proof.
(* Goal: @join_hom (prod nat (_functor KI.F predicate)) Join_nat_F (prod nat (_functor KI.F predicate)) Join_nat_F (@compose (prod nat (_functor KI.F predicate)) knot (prod nat (_functor KI.F predicate)) unsquash squash) *)
    unfold compose.
(* Goal: @join_hom (prod nat (_functor KI.F predicate)) Join_nat_F (prod nat (_functor KI.F predicate)) Join_nat_F (fun x : prod nat (_functor KI.F predicate) => unsquash (squash x)) *)
    intros [x1 x2] [y1 y2] [z1 z2] ?.
(* Goal: @join (prod nat (_functor KI.F predicate)) Join_nat_F (unsquash (squash (@pair nat (_functor KI.F predicate) x1 x2))) (unsquash (squash (@pair nat (_functor KI.F predicate) y1 y2))) (unsquash (squash (@pair nat (_functor KI.F predicate) z1 z2))) *)
    do 3 rewrite (unsquash_squash).
(* Goal: @join (prod nat (_functor KI.F predicate)) Join_nat_F (@pair nat (_functor KI.F predicate) x1 (@fmap KI.F predicate predicate (approx x1) (approx x1) x2)) (@pair nat (_functor KI.F predicate) y1 (@fmap KI.F predicate predicate (approx y1) (approx y1) y2)) (@pair nat (_functor KI.F predicate) z1 (@fmap KI.F predicate predicate (approx z1) (approx z1) z2)) *)
    firstorder.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    simpl in *.
(* Goal: @join (_functor F predicate) (Join_F predicate) (@fmap KI.F predicate predicate (approx x1) (approx x1) x2) (@fmap KI.F predicate predicate (approx y1) (approx y1) y2) (@fmap KI.F predicate predicate (approx z1) (approx z1) z2) *)
    subst y1.
(* Goal: @join (_functor F predicate) (Join_F predicate) (@fmap KI.F predicate predicate (approx x1) (approx x1) x2) (@fmap KI.F predicate predicate (approx x1) (approx x1) y2) (@fmap KI.F predicate predicate (approx z1) (approx z1) z2) *)
    subst z1.
(* Goal: @join (_functor F predicate) (Join_F predicate) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wx) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy) (@fmap K.KI.F K.predicate K.predicate (K.approx (S n)) (K.approx (S n)) f) *)
(* Goal: and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx))) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy))) (@Some knot y')) *)
    apply (paf_join_hom paf_F); auto.
  Qed.

  Instance Join_knot : Join knot :=
           Join_preimage knot (nat * F predicate) Join_nat_F unsquash.

  Lemma join_unsquash : forall x1 x2 x3,
    join x1 x2 x3 =
    join (unsquash x1) (unsquash x2) (unsquash x3).
  Proof.
(* Goal: forall x1 x2 x3 : knot, @eq Prop (@join knot Join_knot x1 x2 x3) (@join (prod nat (_functor KI.F predicate)) Join_nat_F (unsquash x1) (unsquash x2) (unsquash x3)) *)
    intuition.
  Qed.

  Instance Perm_knot : Perm_alg knot :=
    Perm_preimage _ _ _ _ unsquash squash squash_unsquash unsquash_squash_join_hom.

  Instance Sep_knot: Sep_alg knot :=
    Sep_preimage _ _ _  unsquash squash squash_unsquash unsquash_squash_join_hom.

  Lemma core_unsquash : forall x, core x = squash (core (unsquash x)).
  Proof.
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    auto.
  Qed.

  Lemma age_join1 :
    forall x y z x' : K'.knot,
      join x y z ->
      age x x' ->
      exists y' : K'.knot,
        exists z' : K'.knot, join x' y' z' /\ age y y' /\ age z z'.
  Proof.
(* Goal: forall (z x' y' z' : knot) (_ : @join knot Join_knot x' y' z') (_ : @age knot K.ageable_knot z z'), @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
    intros.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    unfold age in *; simpl in *.
(* Goal: None *)
    rewrite knot_age1 in H0.
(* Goal: forall (_ : Join_nat_F (unsquash x') (unsquash y') (unsquash z')) (_ : @eq (option knot) (@age1 knot K.ageable_knot z) (@Some knot z')), @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (unsquash z)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    repeat rewrite knot_age1.
(* Goal: None *)
    do 3 red in H.
(* Goal: None *)
    destruct (unsquash x) as [n f].
(* Goal: None *)
    destruct (unsquash y) as [n0 f0].
(* Goal: None *)
    destruct (unsquash z) as [n1 f1].
(* Goal: None *)
    destruct n; try discriminate.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    inv H0.
(* Goal: None *)
    simpl in H; destruct H.
(* Goal: None *)
    simpl in H; destruct H.
(* Goal: None *)
    subst n0 n1.
(* Goal: None *)
    exists (squash (n,f0)).
(* Goal: None *)
    exists (squash (n,f1)).
(* Goal: None *)
    simpl in H0.
(* Goal: forall x1 x2 x3 : knot, @eq Prop (@join knot Join_knot x1 x2 x3) (@join (prod nat (_functor KI.F predicate)) Join_nat_F (unsquash x1) (unsquash x2) (unsquash x3)) *)
    split; intuition. do 3  red.
(* Goal: and (@join nat (Join_equiv nat) (@fst nat (_functor F predicate) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx)))) (@fst nat (_functor F predicate) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy)))) (S n)) (@join (_functor F predicate) (Join_F predicate) (@snd nat (_functor F predicate) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx)))) (@snd nat (_functor F predicate) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy)))) f) *)
(* Goal: and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx))) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy))) (@Some knot y')) *)
    repeat rewrite unsquash_squash.
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    split; auto. simpl snd.
(* Goal: @join (_functor F predicate) (Join_F predicate) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wx) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy) (@fmap K.KI.F K.predicate K.predicate (K.approx (S n)) (K.approx (S n)) f) *)
(* Goal: and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx))) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy))) (@Some knot y')) *)
    apply (paf_join_hom paf_F); auto.
  Qed.

  Lemma age_join2 :
    forall x y z z' : K'.knot,
      join x y z ->
      age z z' ->
      exists x' : K'.knot,
        exists y' : K'.knot, join x' y' z' /\ age x x' /\ age y y'.
  Proof.
(* Goal: forall (z x' y' z' : knot) (_ : @join knot Join_knot x' y' z') (_ : @age knot K.ageable_knot z z'), @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
    intros.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    unfold age in *; simpl in *.
(* Goal: None *)
    rewrite knot_age1 in H0.
(* Goal: forall (_ : Join_nat_F (unsquash x') (unsquash y') (unsquash z')) (_ : @eq (option knot) (@age1 knot K.ageable_knot z) (@Some knot z')), @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (unsquash z)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    repeat rewrite knot_age1.
(* Goal: None *)
    do 3 red in H.
(* Goal: None *)
    destruct (unsquash x) as [n f].
(* Goal: None *)
    destruct (unsquash y) as [n0 f0].
(* Goal: None *)
    destruct (unsquash z) as [n1 f1].
(* Goal: None *)
    destruct n1; try discriminate.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    inv H0.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    destruct H; simpl in *.
(* Goal: None *)
    destruct H; subst.
(* Goal: None *)
    exists (squash (n1,f)).
(* Goal: None *)
    exists (squash (n1,f0)).
(* Goal: forall x1 x2 x3 : knot, @eq Prop (@join knot Join_knot x1 x2 x3) (@join (prod nat (_functor KI.F predicate)) Join_nat_F (unsquash x1) (unsquash x2) (unsquash x3)) *)
    split; intuition. do 3  red.
(* Goal: and (@join nat (Join_equiv nat) (@fst nat (_functor F predicate) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx)))) (@fst nat (_functor F predicate) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy)))) (S n)) (@join (_functor F predicate) (Join_F predicate) (@snd nat (_functor F predicate) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx)))) (@snd nat (_functor F predicate) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy)))) f) *)
(* Goal: and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx))) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy))) (@Some knot y')) *)
    repeat rewrite unsquash_squash.
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    split; auto. simpl snd.
(* Goal: @join (_functor F predicate) (Join_F predicate) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wx) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy) (@fmap K.KI.F K.predicate K.predicate (K.approx (S n)) (K.approx (S n)) f) *)
(* Goal: and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx))) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy))) (@Some knot y')) *)
    apply (paf_join_hom paf_F); auto.
  Qed.

  Lemma unage_join1 : forall x x' y' z', join x' y' z' -> age x x' ->
    exists y, exists z, join x y z /\ age y y' /\ age z z'.
  Proof.
(* Goal: forall (z x' y' z' : knot) (_ : @join knot Join_knot x' y' z') (_ : @age knot K.ageable_knot z z'), @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
    intros.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    unfold join, Join_knot, Join_preimage, age in *; simpl in *.
    revert H0; rewrite knot_age1;
(* Goal: forall (z x' y' z' : knot) (_ : @join knot Join_knot x' y' z') (_ : @age knot K.ageable_knot z z'), @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
    destruct (unsquash x) as [n f] eqn:?H; intros.
(* Goal: @ex knot (fun y : knot => @ex knot (fun z : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (@pair nat (_functor KI.F predicate) n f) (unsquash y) (unsquash z)) (and (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y')) (@eq (option knot) (@age1 knot K.ageable_knot z) (@Some knot z'))))) *)
    destruct n; inv H1.
(* Goal: @ex knot (fun y : knot => @ex knot (fun z : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (@pair nat (_functor KI.F predicate) (S n) f) (unsquash y) (unsquash z)) (and (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y')) (@eq (option knot) (@age1 knot K.ageable_knot z) (@Some knot z'))))) *)
    hnf in H. rewrite unsquash_squash in H. simpl in H.
(* Goal: @ex knot (fun y : knot => @ex knot (fun z : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (@pair nat (_functor KI.F predicate) (S n) f) (unsquash y) (unsquash z)) (and (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y')) (@eq (option knot) (@age1 knot K.ageable_knot z) (@Some knot z'))))) *)
    revert H.
(* Goal: forall _ : and (@join nat (Join_equiv nat) n (@fst nat (_functor F predicate) (unsquash y')) (@fst nat (_functor F predicate) (unsquash z'))) (@join (_functor F predicate) (Join_F predicate) (@fmap KI.F predicate predicate (approx n) (approx n) f) (@snd nat (_functor F predicate) (unsquash y')) (@snd nat (_functor F predicate) (unsquash z'))), @ex knot (fun y : knot => @ex knot (fun z : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (@pair nat (_functor KI.F predicate) (S n) f) (unsquash y) (unsquash z)) (and (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y')) (@eq (option knot) (@age1 knot K.ageable_knot z) (@Some knot z'))))) *)
    destruct (unsquash y') as [n1 f1] eqn:?H.
(* Goal: forall (z x' y' z' : knot) (_ : @join knot Join_knot x' y' z') (_ : @age knot K.ageable_knot z z'), @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
    destruct (unsquash z') as [n0 f0] eqn:?H; intros.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    destruct H2; simpl in *.
(* Goal: @ex knot (fun y : knot => @ex knot (fun z : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (@pair nat (_functor KI.F predicate) (S n) f) (unsquash y) (unsquash z)) (and (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y')) (@eq (option knot) (@age1 knot K.ageable_knot z) (@Some knot z'))))) *)
    destruct H2; subst.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n0) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    rename n0 into n.
    destruct (paf_preserves_unmap_right paf_F (approx n) (approx n) f f1 f0)
      as [q [w [? [? ?]]]].
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    rewrite <- (unsquash_approx H); auto.
(* Goal: @ex knot (fun y : knot => @ex knot (fun z : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (@pair nat (_functor KI.F predicate) (S n) f) (unsquash y) (unsquash z)) (and (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y')) (@eq (option knot) (@age1 knot K.ageable_knot z) (@Some knot z'))))) *)
    exists (squash (S n,q)).
(* Goal: @ex knot (fun z : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (@pair nat (_functor KI.F predicate) (S n) f) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) q))) (unsquash z)) (and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) q))) (@Some knot y')) (@eq (option knot) (@age1 knot K.ageable_knot z) (@Some knot z')))) *)
    exists (squash (S n,w)). split. hnf.
(* Goal: and (@join nat (Join_equiv nat) (@fst nat (_functor F predicate) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx)))) (@fst nat (_functor F predicate) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy)))) (S n)) (@join (_functor F predicate) (Join_F predicate) (@snd nat (_functor F predicate) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx)))) (@snd nat (_functor F predicate) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy)))) f) *)
(* Goal: and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx))) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy))) (@Some knot y')) *)
    repeat rewrite unsquash_squash.
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    split; simpl; auto.
(* Goal: @join (_functor F predicate) (Join_F predicate) f (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) q) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) w) *)
(* Goal: and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) q))) (@Some knot y')) (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) w))) (@Some knot z')) *)
    generalize (paf_join_hom paf_F (approx (S n)) (approx (S n)) _ _ _ H2).
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    rewrite <- (unsquash_approx H0); auto.

(* Goal: @join (prod nat (_functor F predicate)) Join_nat_F (@pair nat (_functor KI.F predicate) (S n) f) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) q))) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) w))) *)
(* Goal: and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) q))) (@Some knot y')) (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) w))) (@Some knot z')) *)
    split; hnf.
(* Goal: @eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) w))) (@Some knot z') *)
    rewrite knot_age1.
(* Goal: @eq (option knot) (let (n0, x) := unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) w)) in match n0 with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor KI.F predicate) n x)) end) (@Some knot z') *)
    rewrite unsquash_squash. f_equal.
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    replace y' with (squash (n, fmap F (approx (S n)) (approx (S n)) q)); auto.
(* Goal: @eq knot (squash (@pair nat (_functor KI.F predicate) n (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy))) y' *)
    apply unsquash_inj.
(* Goal: @eq (prod nat (_functor K.KI.F K.predicate)) (K.unsquash (squash (@pair nat (_functor F predicate) n (@fmap F predicate predicate (approx (S n)) (approx (S n)) q)))) (K.unsquash y') *)
(* Goal: @eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) w))) (@Some knot z') *)
    rewrite unsquash_squash, H.
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    apply injective_projections; simpl; auto.
(* Goal: @join (_functor F predicate) (Join_F predicate) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wx) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy) f *)
(* Goal: and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx))) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy))) (@Some knot y')) *)
    rewrite (unsquash_approx H).
(* Goal: @eq (_functor K.KI.F K.predicate) (@fmap KI.F predicate predicate (approx n) (approx n) (@fmap F predicate predicate (approx (S n)) (approx (S n)) q)) (@fmap K.KI.F K.predicate K.predicate (K.approx n) (K.approx n) f1) *)
(* Goal: @eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) w))) (@Some knot z') *)
    rewrite <- H4.
(* Goal: @eq (_functor K.KI.F K.predicate) (@fmap KI.F predicate predicate (approx n) (approx n) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy)) f1 *)
    rewrite fmap_app.
    replace (approx n oo approx (S n)) with (approx n);
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    [replace (approx (S n) oo approx n) with (approx n) |]; auto.
(* Goal: @eq (forall _ : predicate, predicate) (approx n) (@compose predicate predicate predicate (approx n) (approx (S n))) *)
    extensionality a.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx n) (approx (S n)) a) *)
    replace (S n) with (1 + n)%nat by trivial.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx (Init.Nat.add (S O) n)) (approx n) a) *)
(* Goal: @eq (forall _ : predicate, predicate) (approx n) (@compose predicate predicate predicate (approx n) (approx (S n))) *)
    rewrite <- (approx_approx2 1 n).
(* Goal: @eq predicate (approx n a) (K.approx n a) *)
    trivial.
(* Goal: @eq (forall _ : predicate, predicate) (approx n) (@compose predicate predicate predicate (approx n) (approx (S n))) *)
    extensionality a.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx n) (approx (S n)) a) *)
    replace (S n) with (1 + n)%nat by trivial.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx n) (approx (Init.Nat.add (S O) n)) a) *)
    rewrite <- (approx_approx1 1 n).
(* Goal: @eq predicate (approx n a) (K.approx n a) *)
    trivial.

(* Goal: @eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) w))) (@Some knot z') *)
    rewrite knot_age1.
(* Goal: @eq (option knot) (let (n0, x) := unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) w)) in match n0 with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor KI.F predicate) n x)) end) (@Some knot z') *)
    rewrite unsquash_squash. f_equal.
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    replace z' with  (squash (n,fmap F (approx (S n)) (approx (S n)) w)); auto.
(* Goal: @eq knot (squash (@pair nat (_functor KI.F predicate) n (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy))) y' *)
    apply unsquash_inj.
(* Goal: @eq (prod nat (_functor K.KI.F K.predicate)) (K.unsquash (squash (@pair nat (_functor KI.F predicate) n (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy)))) (K.unsquash y') *)
    rewrite unsquash_squash, H1.
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    apply injective_projections; simpl; auto.
(* Goal: @eq (_functor K.KI.F K.predicate) (@fmap KI.F predicate predicate (approx n) (approx n) (@fmap F predicate predicate (approx (S n)) (approx (S n)) w)) f0 *)
    rewrite <- H5.
(* Goal: @eq (_functor K.KI.F K.predicate) (@fmap KI.F predicate predicate (approx n) (approx n) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy)) f1 *)
    rewrite fmap_app.
    replace (approx n oo approx (S n)) with (approx n);
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    [replace (approx (S n) oo approx n) with (approx n) |]; auto.
(* Goal: @eq (forall _ : predicate, predicate) (approx n) (@compose predicate predicate predicate (approx n) (approx (S n))) *)
    extensionality a.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx n) (approx (S n)) a) *)
    replace (S n) with (1 + n)%nat by trivial.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx (Init.Nat.add (S O) n)) (approx n) a) *)
(* Goal: @eq (forall _ : predicate, predicate) (approx n) (@compose predicate predicate predicate (approx n) (approx (S n))) *)
    rewrite <- (approx_approx2 1 n).
(* Goal: @eq predicate (approx n a) (K.approx n a) *)
    trivial.
(* Goal: @eq (forall _ : predicate, predicate) (approx n) (@compose predicate predicate predicate (approx n) (approx (S n))) *)
    extensionality a.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx n) (approx (S n)) a) *)
    replace (S n) with (1 + n)%nat by trivial.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx n) (approx (Init.Nat.add (S O) n)) a) *)
    rewrite <- (approx_approx1 1 n).
(* Goal: @eq predicate (approx n a) (K.approx n a) *)
    trivial.
  Qed.

  Lemma unage_join2 :
    forall z x' y' z', join x' y' z' -> age z z' ->
      exists x, exists y, join x y z /\ age x x' /\ age y y'.
  Proof.
(* Goal: forall (z x' y' z' : knot) (_ : @join knot Join_knot x' y' z') (_ : @age knot K.ageable_knot z z'), @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
    intros.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
    rewrite join_unsquash in H.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
    revert H H0.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    unfold join, Join_knot, Join_preimage, age in *; simpl in *.
(* Goal: forall (_ : Join_nat_F (unsquash x') (unsquash y') (unsquash z')) (_ : @eq (option knot) (@age1 knot K.ageable_knot z) (@Some knot z')), @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (unsquash z)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    repeat rewrite knot_age1.

    destruct (unsquash z) as [n f] eqn:?H;
    destruct (unsquash z') as [n0 f0] eqn:?H;
    destruct (unsquash y') as [n1 f1] eqn:?H;
(* Goal: forall (z x' y' z' : knot) (_ : @join knot Join_knot x' y' z') (_ : @age knot K.ageable_knot z z'), @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
    destruct (unsquash x') as [n2 f2] eqn:?H; intros.
    destruct n;  inv H4.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    destruct H3. hnf in H3. simpl in *. destruct H3; subst.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    rewrite unsquash_squash in H0.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    inv H0.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n0) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    rename n0 into n.

    destruct (paf_preserves_unmap_left paf_F
      (approx n) (approx n) f2 f1 f)
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
      as [wx [wy [? [? ?]]]]; auto.
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    rewrite <- (unsquash_approx H1); auto.
(* Goal: @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash x) (unsquash y) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot x) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y'))))) *)
    exists (squash (S n, wx)).
(* Goal: @ex knot (fun y : knot => and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx))) (unsquash y) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx))) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot y) (@Some knot y')))) *)
    exists (squash (S n, wy)).
(* Goal: and (@join (prod nat (_functor F predicate)) Join_nat_F (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx))) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy))) (@pair nat (_functor KI.F predicate) (S n) f)) (and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx))) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy))) (@Some knot y'))) *)
    split. unfold join, Join_nat_F, Join_prod; simpl.
(* Goal: and (@join nat (Join_equiv nat) (@fst nat (_functor F predicate) (@pair nat (_functor KI.F predicate) (S n) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wx))) (@fst nat (_functor F predicate) (@pair nat (_functor KI.F predicate) (S n) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy))) (S n)) (@join (_functor F predicate) (Join_F predicate) (@snd nat (_functor F predicate) (@pair nat (_functor KI.F predicate) (S n) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wx))) (@snd nat (_functor F predicate) (@pair nat (_functor KI.F predicate) (S n) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy))) f) *)
(* Goal: and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx))) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy))) (@Some knot y')) *)
    (* unfold Join_knot; simpl. unfold Join_preimage; simpl. *)
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    repeat rewrite unsquash_squash.  simpl.  split; auto.

(* Goal: @join (_functor F predicate) (Join_F predicate) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wx) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy) f *)
(* Goal: and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx))) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy))) (@Some knot y')) *)
    rewrite (unsquash_approx H).
(* Goal: @join (_functor F predicate) (Join_F predicate) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wx) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy) (@fmap K.KI.F K.predicate K.predicate (K.approx (S n)) (K.approx (S n)) f) *)
(* Goal: and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wx))) (@Some knot x')) (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) wy))) (@Some knot y')) *)
    apply (paf_join_hom paf_F); auto.
(* Goal: @join (prod nat (_functor F predicate)) Join_nat_F (@pair nat (_functor KI.F predicate) (S n) f) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) q))) (unsquash (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) w))) *)
(* Goal: and (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) q))) (@Some knot y')) (@eq (option knot) (@age1 knot K.ageable_knot (squash (@pair nat (_functor KSAI.KI.F predicate) (S n) w))) (@Some knot z')) *)
    split; rewrite knot_age1; rewrite unsquash_squash; f_equal; hnf.
(* Goal: @eq knot (squash (@pair nat (_functor KI.F predicate) n (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy))) y' *)
    apply unsquash_inj.
(* Goal: @eq (prod nat (_functor K.KI.F K.predicate)) (K.unsquash (squash (@pair nat (_functor KI.F predicate) n (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wx)))) (K.unsquash x') *)
(* Goal: @eq knot (squash (@pair nat (_functor KI.F predicate) n (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy))) y' *)
    rewrite unsquash_squash, H2.
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    apply injective_projections; simpl; auto.
(* Goal: @eq (_functor K.KI.F K.predicate) (@fmap KI.F predicate predicate (approx n) (approx n) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy)) f1 *)
    rewrite fmap_app.
    replace (approx n oo approx (S n)) with (approx n);
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    [replace (approx (S n) oo approx n) with (approx n) |]; auto.
(* Goal: @eq (forall _ : predicate, predicate) (approx n) (@compose predicate predicate predicate (approx n) (approx (S n))) *)
    extensionality a.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx n) (approx (S n)) a) *)
    replace (S n) with (1 + n)%nat by trivial.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx (Init.Nat.add (S O) n)) (approx n) a) *)
(* Goal: @eq (forall _ : predicate, predicate) (approx n) (@compose predicate predicate predicate (approx n) (approx (S n))) *)
    rewrite <- (approx_approx2 1 n).
(* Goal: @eq predicate (approx n a) (K.approx n a) *)
    trivial.
(* Goal: @eq (forall _ : predicate, predicate) (approx n) (@compose predicate predicate predicate (approx n) (approx (S n))) *)
    extensionality a.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx n) (approx (S n)) a) *)
    replace (S n) with (1 + n)%nat by trivial.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx n) (approx (Init.Nat.add (S O) n)) a) *)
    rewrite <- (approx_approx1 1 n).
(* Goal: @eq predicate (approx n a) (K.approx n a) *)
    trivial.

(* Goal: @eq knot (squash (@pair nat (_functor KI.F predicate) n (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy))) y' *)
    apply unsquash_inj.
(* Goal: @eq (prod nat (_functor K.KI.F K.predicate)) (K.unsquash (squash (@pair nat (_functor KI.F predicate) n (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy)))) (K.unsquash y') *)
    rewrite unsquash_squash, H1.
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    apply injective_projections; simpl; auto.
(* Goal: @eq (_functor K.KI.F K.predicate) (@fmap KI.F predicate predicate (approx n) (approx n) (@fmap KI.F predicate predicate (approx (S n)) (approx (S n)) wy)) f1 *)
    rewrite fmap_app.
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    rewrite (unsquash_approx H1), <- H5; auto.
    replace (approx n oo approx (S n)) with (approx n);
(* Goal: forall x : knot, @eq knot (@core knot Join_knot Sep_knot x) (squash (@core (prod nat (_functor KI.F predicate)) Join_nat_F Sep_nat_F (unsquash x))) *)
    [replace (approx (S n) oo approx n) with (approx n) |]; auto.
(* Goal: @eq (forall _ : predicate, predicate) (approx n) (@compose predicate predicate predicate (approx n) (approx (S n))) *)
    extensionality a.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx n) (approx (S n)) a) *)
    replace (S n) with (1 + n)%nat by trivial.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx (Init.Nat.add (S O) n)) (approx n) a) *)
(* Goal: @eq (forall _ : predicate, predicate) (approx n) (@compose predicate predicate predicate (approx n) (approx (S n))) *)
    rewrite <- (approx_approx2 1 n).
(* Goal: @eq predicate (approx n a) (K.approx n a) *)
    trivial.
(* Goal: @eq (forall _ : predicate, predicate) (approx n) (@compose predicate predicate predicate (approx n) (approx (S n))) *)
    extensionality a.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx n) (approx (S n)) a) *)
    replace (S n) with (1 + n)%nat by trivial.
(* Goal: @eq predicate (approx n a) (@compose predicate predicate predicate (approx n) (approx (Init.Nat.add (S O) n)) a) *)
    rewrite <- (approx_approx1 1 n).
(* Goal: @eq predicate (approx n a) (K.approx n a) *)
    trivial.
  Qed.

  Theorem asa_knot : @Age_alg knot _ K.ageable_knot.
  Proof.
(* Goal: @Age_alg knot Join_knot K.ageable_knot *)
    constructor.
(* Goal: forall (x y z x' : knot) (_ : @join knot Join_knot x y z) (_ : @age knot K.ageable_knot x x'), @ex knot (fun y' : knot => @ex knot (fun z' : knot => and (@join knot Join_knot x' y' z') (and (@age knot K.ageable_knot y y') (@age knot K.ageable_knot z z')))) *)
(* Goal: forall (x y z z' : knot) (_ : @join knot Join_knot x y z) (_ : @age knot K.ageable_knot z z'), @ex knot (fun x' : knot => @ex knot (fun y' : knot => and (@join knot Join_knot x' y' z') (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
(* Goal: forall (x x' y' z' : knot) (_ : @join knot Join_knot x' y' z') (_ : @age knot K.ageable_knot x x'), @ex knot (fun y : knot => @ex knot (fun z : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot y y') (@age knot K.ageable_knot z z')))) *)
(* Goal: forall (z x' y' z' : knot) (_ : @join knot Join_knot x' y' z') (_ : @age knot K.ageable_knot z z'), @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
    exact age_join1.
(* Goal: forall (x y z z' : knot) (_ : @join knot Join_knot x y z) (_ : @age knot K.ageable_knot z z'), @ex knot (fun x' : knot => @ex knot (fun y' : knot => and (@join knot Join_knot x' y' z') (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
(* Goal: forall (x x' y' z' : knot) (_ : @join knot Join_knot x' y' z') (_ : @age knot K.ageable_knot x x'), @ex knot (fun y : knot => @ex knot (fun z : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot y y') (@age knot K.ageable_knot z z')))) *)
(* Goal: forall (z x' y' z' : knot) (_ : @join knot Join_knot x' y' z') (_ : @age knot K.ageable_knot z z'), @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
    exact age_join2.
(* Goal: forall (x x' y' z' : knot) (_ : @join knot Join_knot x' y' z') (_ : @age knot K.ageable_knot x x'), @ex knot (fun y : knot => @ex knot (fun z : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot y y') (@age knot K.ageable_knot z z')))) *)
(* Goal: forall (z x' y' z' : knot) (_ : @join knot Join_knot x' y' z') (_ : @age knot K.ageable_knot z z'), @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
    exact unage_join1.
(* Goal: forall (z x' y' z' : knot) (_ : @join knot Join_knot x' y' z') (_ : @age knot K.ageable_knot z z'), @ex knot (fun x : knot => @ex knot (fun y : knot => and (@join knot Join_knot x y z) (and (@age knot K.ageable_knot x x') (@age knot K.ageable_knot y y')))) *)
    exact unage_join2.
  Qed.

End KnotFullSa.
