Require Import VST.msl.base.
Require Import VST.msl.ageable.
Require Import VST.msl.functors.
Import VST.msl.functors.MixVariantFunctor.
Import VST.msl.functors.MixVariantFunctorLemmas.

Module Type KNOT_INPUT__MIXVARIANT_HERED_T_OTH_REL.
  Parameter F : functor.

  Parameter other : Type.

  Parameter Rel : forall A, F A -> F A -> Prop.

  Parameter Rel_fmap : forall A B (f1: A->B) (f2:B->A) x y,
    Rel A x y ->
    Rel B (fmap F f1 f2 x) (fmap F f1 f2 y).
  Axiom Rel_refl : forall A x, Rel A x x.
  Axiom Rel_trans : forall A x y z,
    Rel A x y -> Rel A y z -> Rel A x z.

  Parameter ORel : other -> other -> Prop.
  Axiom ORel_refl : reflexive other ORel.
  Axiom ORel_trans : transitive other ORel.

  Parameter T:Type.
  Parameter T_bot:T.

  Parameter T_rel : T -> T -> Prop.
  Parameter T_rel_bot : forall x, T_rel T_bot x.
  Parameter T_rel_refl : forall x, T_rel x x.
  Parameter T_rel_trans : transitive T T_rel.

End KNOT_INPUT__MIXVARIANT_HERED_T_OTH_REL.

Module Type KNOT__MIXVARIANT_HERED_T_OTH_REL.
  Declare Module KI: KNOT_INPUT__MIXVARIANT_HERED_T_OTH_REL.
  Import KI.

  Parameter knot:Type.
  Parameter ageable_knot : ageable knot.
  Existing Instance ageable_knot.

  Parameter hered : (knot * other -> T) -> Prop.
  Definition predicate := { p:knot * other -> T | hered p }.

  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 approx_spec : forall n p ko,
    proj1_sig (approx n p) ko =
     if (le_gt_dec n (level (fst ko))) then T_bot else proj1_sig p ko.

  Definition knot_rel (k1 k2:knot) :=
    let (n,f) := unsquash k1 in
    let (n',f') := unsquash k2 in
    n = n' /\ Rel predicate f 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).

  Axiom hered_spec : forall p,
    hered p =
    (forall k k' k'' o o',
      clos_refl_trans _ age k k' ->
      knot_rel  k' k'' ->
      ORel o o' ->
      T_rel (p (k,o)) (p (k'',o'))).

End KNOT__MIXVARIANT_HERED_T_OTH_REL.

Module Knot_MixVariantHeredTOthRel (KI':KNOT_INPUT__MIXVARIANT_HERED_T_OTH_REL) :
  KNOT__MIXVARIANT_HERED_T_OTH_REL with Module KI:=KI'.
  Module KI := KI'.
  Import KI.

  Definition sinv_prod X := prod X (F X * other -> T).

  Definition guppy_sig := (fun X:Type => X * (F X * other -> T) -> Prop).
  Definition guppy_ty := sigT guppy_sig.

  Definition guppy_step_ty (Z:guppy_ty) : Type :=
    (sig (fun (x:sinv_prod (projT1 Z)) => projT2 Z x)).

  Definition guppy_age (Z:guppy_ty) (x:guppy_step_ty Z) : projT1 Z := fst (proj1_sig x).
  Definition guppy_unage (Z:guppy_ty)
    (H:forall t, projT2 Z (t,fun _ => T_bot))
    (x:projT1 Z) : guppy_step_ty Z :=
    exist (fun z => projT2 Z z) (x, fun _ => T_bot) (H x).

  Definition guppy_step_prop (Z:guppy_ty) (xf:sinv_prod (guppy_step_ty Z)) :=
    (forall (k:F (guppy_step_ty Z)) (o:other) H,
         T_rel (snd xf (k,o))
               (snd (proj1_sig (fst xf)) (fmap F (guppy_age Z) (guppy_unage Z H) k,o))) /\
    (forall (k k':F (guppy_step_ty Z)) (o o':other),
         Rel (guppy_step_ty Z) k k' ->
         ORel o o' ->
         T_rel (snd xf (k,o)) (snd xf (k',o'))).

  Definition guppy_step (Z:guppy_ty) : guppy_ty :=
    existT guppy_sig (guppy_step_ty Z) (guppy_step_prop Z).

  Definition guppy_base : guppy_ty :=
    existT guppy_sig unit
      (fun xf =>
        (forall (k k':F unit) (o o':other),
          Rel unit k k' ->
          ORel o o' ->
          T_rel (snd xf (k,o)) (snd xf (k',o')))).

  Fixpoint guppy (n:nat) : guppy_ty :=
    match n with
    | 0    => guppy_base
    | S n' => guppy_step (guppy n')
    end.

  Definition sinv (n:nat) : Type := projT1 (guppy n).
  Definition sinv_prop (n:nat) : prod (sinv n) (F (sinv n) * other -> T) -> Prop := projT2 (guppy n).

  Fixpoint floor (m:nat) (n:nat) (p:sinv (m+n)) : sinv n :=
    match m as m' return forall (p : sinv (m'+n)), sinv n with
    | O => fun p => p
    | S m' => fun p => floor m' n (fst (proj1_sig p))
    end p.

  Definition knot := { n:nat & F (sinv n) }.

  Definition sinv_age n : sinv (S n) -> sinv n := guppy_age (guppy n).
  Program Definition sinv_unage n : sinv n -> sinv (S n) := guppy_unage (guppy n) _.
  Next Obligation.
(* Goal: @projT2 Type guppy_sig (guppy n) (@pair (@projT1 Type guppy_sig (guppy n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy n))) other, T) t (fun _ : prod (_functor F (@projT1 Type guppy_sig (guppy n))) other => T_bot)) *)
    revert t; induction n; simpl; auto.
(* Goal: forall (_ : unit) (k k' : _functor F unit) (o o' : other) (_ : Rel unit k k') (_ : ORel o o'), T_rel T_bot T_bot *)
(* Goal: forall t : guppy_step_ty (guppy n), guppy_step_prop (guppy n) (@pair (guppy_step_ty (guppy n)) (forall _ : prod (_functor F (guppy_step_ty (guppy n))) other, T) t (fun _ : prod (_functor F (guppy_step_ty (guppy n))) other => T_bot)) *)
    repeat intro.
(* Goal: T_rel T_bot (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    apply T_rel_bot.
(* Goal: forall (_ : unit) (k k' : _functor F unit) (o o' : other) (_ : Rel unit k k') (_ : ORel o o'), T_rel T_bot T_bot *)
(* Goal: forall t : guppy_step_ty (guppy n), guppy_step_prop (guppy n) (@pair (guppy_step_ty (guppy n)) (forall _ : prod (_functor F (guppy_step_ty (guppy n))) other, T) t (fun _ : prod (_functor F (guppy_step_ty (guppy n))) other => T_bot)) *)
    split; simpl in *; repeat intro.
(* Goal: T_rel T_bot (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    apply T_rel_bot.
(* Goal: T_rel T_bot (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    apply T_rel_bot.
  Qed.

  Definition F_sinv n := F (sinv n).

  Definition age1_def (k:knot) : option knot :=
    match k with
      | existT _ 0 f => None
      | existT _ (S m) f => Some
          (existT F_sinv m (fmap F (sinv_age m) (sinv_unage m) f))
    end.

  Definition age_def x y := age1_def x = Some y.

  Inductive knot_rel_inner : knot -> knot -> Prop :=
    | intro_krel : forall n (f f':F_sinv n),
         Rel _ f f' ->
         knot_rel_inner (existT (F_sinv) n f) (existT (F_sinv) n f').

  Definition hered (p:knot * other -> T) : Prop :=
    forall k k' k'' o o',
      clos_refl_trans _ age_def k k' ->
      knot_rel_inner k' k'' -> ORel o o' ->
      T_rel (p (k,o)) (p (k'',o')).

  Definition predicate := { p:knot * other -> T | hered p }.

  Definition app_sinv (n:nat) (p:sinv (S n)) (x:F_sinv n * other) :=
    snd (proj1_sig p) x.

  Section stratifies.
    Variable Q:knot * other -> T.
    Variable HQ:hered Q.

    Fixpoint stratifies (n:nat) : sinv n -> Prop :=
    match n as n' return sinv n' -> Prop with
    | 0 => fun _ => True
    | S n' => fun (p:sinv (S n')) =>
          stratifies n' (fst (proj1_sig p)) /\
          forall (k:F_sinv n') (o:other), snd (proj1_sig p) (k,o) = Q (existT F_sinv n' k,o)
    end.

    Lemma stratifies_unique : forall n p1 p2,
      stratifies n p1 ->
      stratifies n p2 ->
      p1 = p2.
    Proof.
(* Goal: forall (n : nat) (p1 p2 : sinv n) (_ : stratifies n p1) (_ : stratifies n p2), @eq (sinv n) p1 p2 *)
      induction n; simpl; intuition.
(* Goal: @eq (sinv O) p1 p2 *)
(* Goal: @eq (sinv (S n)) p1 p2 *)
      destruct p1; destruct p2; auto.
(* Goal: @eq (sinv (S n)) p1 p2 *)
      destruct p1; destruct p2.
(* Goal: @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
      simpl in *; fold guppy in *.
(* Goal: @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
      cut (x = x0).
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
      intros.
(* Goal: @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
(* Goal: @eq (sinv_prod (@projT1 Type guppy_sig (guppy n))) x x0 *)
      revert p p0 H2 H3.
(* Goal: forall (p : @projT2 Type guppy_sig (guppy n) x) (p0 : @projT2 Type guppy_sig (guppy n) x0) (_ : forall (k : F_sinv n) (o : other), @eq T (@snd (@projT1 Type guppy_sig (guppy n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy n))) other, T) x (@pair (F_sinv n) other k o)) (Q (@pair (@sigT nat F_sinv) other (@existT nat F_sinv n k) o))) (_ : forall (k : F_sinv n) (o : other), @eq T (@snd (@projT1 Type guppy_sig (guppy n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy n))) other, T) x0 (@pair (F_sinv n) other k o)) (Q (@pair (@sigT nat F_sinv) other (@existT nat F_sinv n k) o))), @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
(* Goal: @eq (sinv_prod (@projT1 Type guppy_sig (guppy n))) x x0 *)
      rewrite <- H0.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
      intros.
(* Goal: @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p0) *)
(* Goal: @eq (sinv_prod (@projT1 Type guppy_sig (guppy n))) x x0 *)
      replace p0 with p by (apply proof_irr); auto.
(* Goal: @eq (sinv_prod (@projT1 Type guppy_sig (guppy n))) x x0 *)
      destruct x; destruct x0; simpl in *.
(* Goal: @eq (sinv_prod (@projT1 Type guppy_sig (guppy n))) (@pair (@projT1 Type guppy_sig (guppy n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy n))) other, T) p1 t) (@pair (@projT1 Type guppy_sig (guppy n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy n))) other, T) p2 t0) *)
      apply injective_projections; simpl.
(* Goal: @eq (@projT1 Type guppy_sig (guppy n)) p1 p2 *)
(* Goal: @eq (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy n))) other, T) t t0 *)
      apply IHn; auto.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
      extensionality; intros.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
      simpl in *.
(* Goal: @eq T (t x) (t0 x) *)
      destruct x as [x o].
(* Goal: @eq T (t (@pair (_functor F (@projT1 Type guppy_sig (guppy n))) other x o)) (t0 (@pair (_functor F (@projT1 Type guppy_sig (guppy n))) other x o)) *)
      destruct (H2 x o); destruct (H3 x o).
(* Goal: @eq (@Fpred kli) (@approxF kli n Fp) (@approxF kli n (@approxF kli n Fp)) *)
      rewrite H2.
(* Goal: @eq T (Q (@pair (@sigT nat F_sinv) other (@existT nat F_sinv n x) o)) (t0 (@pair (_functor F (@projT1 Type guppy_sig (guppy n))) other x o)) *)
      rewrite H3.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
      auto.
    Qed.

    Definition stratify (n:nat) : { x:sinv n | stratifies n x }.
    Proof.
      induction n.
      exists tt; simpl; exact I.
      assert (HX:
        projT2 (guppy n)
        (proj1_sig IHn, fun v : F_sinv n * other => Q (existT F_sinv n (fst v),snd v))).
      destruct n.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
      simpl; intros.
      eapply HQ.
      apply rt_refl.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
      constructor; auto.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
      auto.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
      simpl; intros.
      destruct IHn; simpl.
      simpl in s; destruct s.
(* Goal: @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
      destruct x; simpl in *; fold guppy in *.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
      destruct x; simpl in *.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
      split; hnf; simpl; intros.
      rewrite H0.
      eapply HQ.
      apply rt_step.
      hnf; simpl.
      reflexivity.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
      constructor; auto.
      unfold sinv_unage.
      replace (sinv_unage_obligation_1 n) with H1.
      unfold sinv_age.
      apply Rel_refl.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
      apply proof_irr.
      apply ORel_refl.
      eapply HQ.
      apply rt_refl.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
      constructor; auto.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
      auto.

      exists ((exist (fun x => projT2 (guppy n) x) ( proj1_sig IHn, fun v:F_sinv n * other => Q (existT (F_sinv) n (fst v),snd v) ) HX)).
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
      simpl; split; auto.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
      destruct IHn; auto.
    Qed.
  End stratifies.

  Lemma decompose_nat : forall (x y:nat), { m:nat & y = (m + S x) } + { ge x y }.
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros x y; revert x; induction y; simpl; intros.
(* Goal: sumor (@sigT nat (fun m : nat => @eq nat O (Init.Nat.add m (S x)))) (ge x O) *)
(* Goal: sumor (@sigT nat (fun m : nat => @eq nat (S y) (Init.Nat.add m (S x)))) (ge x (S y)) *)
    right; auto with arith.
(* Goal: sumor (@sigT nat (fun m : nat => @eq nat (S y) (Init.Nat.add m (S x)))) (ge x (S y)) *)
    destruct (IHy x) as [[m H]|H].
(* Goal: sumor (@sigT nat (fun m : nat => @eq nat (S y) (Init.Nat.add m (S x)))) (ge x (S y)) *)
(* Goal: sumor (@sigT nat (fun m : nat => @eq nat (S y) (Init.Nat.add m (S x)))) (ge x (S y)) *)
    left; exists (S m); omega.
(* Goal: sumor (@sigT nat (fun m : nat => @eq nat (S y) (Init.Nat.add m (S x)))) (ge x (S y)) *)
    destruct (eq_nat_dec x y).
(* Goal: sumor (@sigT nat (fun m : nat => @eq nat (S y) (Init.Nat.add m (S x)))) (ge x (S y)) *)
(* Goal: sumor (@sigT nat (fun m : nat => @eq nat (S y) (Init.Nat.add m (S x)))) (ge x (S y)) *)
    left; exists O; omega.
(* Goal: sumor (@sigT nat (fun m : nat => @eq nat (S y) (Init.Nat.add m (S x)))) (ge x (S y)) *)
    right; omega.
  Qed.

  Definition unstratify (n:nat) (p:sinv n) : knot * other -> T := fun w =>
    match w with (existT _ nw w',o) =>
      match decompose_nat nw n with
        | inleft (existT _ m Hm) => snd (proj1_sig (floor m (S nw) (eq_rect  n _ p (m + S nw) Hm))) (w',o)
        | inright H => T_bot
      end
    end.

  Lemma floor_shuffle:
    forall (m1 n : nat)
      (p1 : sinv (m1 + S n)) (H1 : (m1 + S n) = (S m1 + n)),
      floor (S m1) n (eq_rect (m1 + S n) sinv p1 (S m1 + n) H1) = fst (proj1_sig (floor m1 (S n) p1)).
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq (sinv n) (floor (S m1) n (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (Init.Nat.add (S m1) n) H1)) (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m1 (S n) p1))) *)
    remember (fst (proj1_sig (floor m1 (S n) p1))) as p.
(* Goal: @eq (sinv n) (floor (S m1) n (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (Init.Nat.add (S m1) n) H1)) p *)
    fold guppy in *.
(* Goal: @eq (sinv n) (floor (S m1) n (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (Init.Nat.add (S m1) n) H1)) p *)
    revert n p1 H1 p Heqp.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    induction m1; simpl; intros.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    replace H1 with (refl_equal (S n)) by (apply proof_irr); simpl; auto.
(* Goal: @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv p1 (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    assert (m1 + S n = S m1 + n) by omega.
(* Goal: @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
    destruct p1 as [[p1 f'] Hp1]; simpl in *; fold guppy in *.
(* Goal: @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@exist (sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) => @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) x) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    generalize (IHm1 n p1 H p Heqp).
(* Goal: forall _ : @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (S (Init.Nat.add m1 n)) H)))) p, @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@exist (sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) => @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) x) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    clear.
(* Goal: forall _ : @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (S (Init.Nat.add m1 n)) H)))) p, @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@exist (sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) => @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) x) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    revert Hp1 H1; generalize H.
(* Goal: forall (H : @eq nat (Init.Nat.add m1 (S n)) (S (Init.Nat.add m1 n))) (Hp1 : @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f')) (H1 : @eq nat (S (Init.Nat.add m1 (S n))) (S (S (Init.Nat.add m1 n)))) (_ : @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (S (Init.Nat.add m1 n)) H)))) p), @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@exist (sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) => @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) x) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    revert p1 f'.
(* Goal: @eq (@knot kli) (@squash kli (@unsquash kli k1)) (@squash kli (@unsquash kli k2)) *)
    rewrite H.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    simpl; intros.
(* Goal: @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (S (Init.Nat.add m1 n))) sinv (@exist (sinv_prod (guppy_step_ty (guppy (Init.Nat.add m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy (Init.Nat.add m1 n))) => guppy_step_prop (guppy (Init.Nat.add m1 n)) x) (@pair (guppy_step_ty (guppy (Init.Nat.add m1 n))) (forall _ : prod (_functor F (guppy_step_ty (guppy (Init.Nat.add m1 n)))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    replace H1 with (refl_equal (S (S (m1 + n)))) by (apply proof_irr).
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
(* Goal: @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) p1))) p *)
    replace H0 with (refl_equal (S (m1+n))) in H2 by (apply proof_irr).
(* Goal: @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) p1))) p *)
    simpl in H2.
(* Goal: @eq (@Fpred kli) (@approxF kli n Fp) Fp *)
    trivial.
  Qed.

  Lemma unstratify_hered : forall n p,
    hered (unstratify n p).
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    hnf; intros.
    apply T_rel_trans with (unstratify n p (k',o)).
    clear o' H0 H1.
    induction H.
    hnf in H; simpl in H.
    destruct x as [x f]; simpl in H.
(* Goal: le (knot_level_def (@existT nat (fun n : nat => _functor F (sinv n)) x0 _f0)) (knot_level_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f)) *)
(* Goal: le (knot_level_def x) (knot_level_def x) *)
(* Goal: le (knot_level_def z) (knot_level_def x) *)
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    destruct x; try discriminate.
    assert (y =
      (existT (F_sinv) x (fmap F (sinv_age x) (sinv_unage x) f))).
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    inversion H; auto.
    subst y.
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) T_bot *)
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x k) *)
    unfold unstratify.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    case_eq (decompose_nat (S x) n); intros.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    case_eq (decompose_nat x n); intros.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
    destruct n.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    elimtype False; omega.
    assert (S x0 = x1) by omega; subst x1.
    revert H1.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    generalize e e0; revert p; rewrite e; intros.
    rewrite floor_shuffle.
    replace e1 with (refl_equal (x0 + S (S x)));
      simpl eq_rect.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    2: apply proof_irr.
    revert H1.
    generalize (floor x0 (S (S x)) p).
(* Goal: @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
    intros [[s' fs] Hs] H1; simpl in *; fold guppy in *.
    destruct Hs.
(* Goal: @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) p1))) p *)
    simpl in H2.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    eapply H2; auto.
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) T_bot *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    elimtype False.
(* Goal: forall _ : le (knot_level_def k'') (knot_level_def k), False *)
(* Goal: le (knot_level_def k'') (knot_level_def k) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    omega.
(* Goal: T_rel T_bot (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    apply T_rel_bot.
    apply T_rel_refl.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    eapply T_rel_trans; eauto.

(* Goal: stratifies (unstratify n p) n p *)
    clear H.
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    inv H0.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
    destruct (decompose_nat n0 n); [ | apply T_rel_bot ].
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    destruct s; simpl.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    destruct (floor x (S n0) (eq_rect n sinv p (x +S n0) e)); simpl.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    destruct n0; simpl in x0; destruct x0; simpl.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    apply p0; auto.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    apply p0; auto.
  Qed.

  Lemma unstratify_Q : forall n (p:sinv n) Q,
    stratifies Q n p ->
    forall (k:knot) (o:other),
      projT1 k < n ->
      (unstratify n p (k,o) = Q (k,o)).
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) T_bot *)
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x k) *)
    unfold unstratify.
(* Goal: @eq T (unstratify n x0 k) (x k) *)
    destruct k.
    destruct (decompose_nat x n).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
    simpl in H0.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    2: simpl in *; elimtype False; omega.
    clear H0.
    revert p H.
    generalize e.
    rewrite e.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    replace e0 with (refl_equal (x0 + S x)) by apply proof_irr.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
    clear e e0.
    revert p H.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    induction x0; simpl; intros.
    destruct H.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.
    destruct H.
    apply IHx0.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.
  Qed.

  Lemma stratifies_unstratify_more :
    forall (n m1 m2:nat) (p1:sinv (m1+n)) (p2:sinv (m2+n)),
      floor m1 n p1 = floor m2 n p2 ->
      (stratifies (unstratify (m1+n) p1) n (floor m1 n p1) ->
       stratifies (unstratify (m2+n) p2) n (floor m2 n p2)).
  Proof.
    induction n; intuition.
    split.
(* Goal: forall _ : le (knot_level_def k'') (knot_level_def k), False *)
(* Goal: le (knot_level_def k'') (knot_level_def k) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    assert (m2 + S n = S m2 + n) by omega.
    erewrite <- floor_shuffle.
    instantiate (1:=H1).
    replace (unstratify (m2 + S n) p2)
      with (unstratify (S m2 + n) (eq_rect (m2 + S n) sinv p2 (S m2 + n) H1)).
(* Goal: @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv p1 (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    assert (m1 + S n = S m1 + n) by omega.
    eapply (IHn (S m1) (S m2)
      (eq_rect (m1 + S n) sinv p1 (S m1 + n) H2)).
    rewrite floor_shuffle.
    rewrite floor_shuffle.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    rewrite H; auto.
    clear - H0.
    rewrite floor_shuffle.
    simpl in H0.
    destruct H0.
    clear H0.
    revert p1 H.
    generalize H2.
    rewrite <- H2.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    replace H0 with (refl_equal (m1 + S n)) by apply proof_irr; auto.
(* Goal: forall _ : @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (S (Init.Nat.add m1 n)) H)))) p, @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@exist (sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) => @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) x) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    clear.
    revert p2.
    generalize H1.
    rewrite H1.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    replace H0 with (refl_equal (S m2 + n)) by apply proof_irr; auto.

(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
    destruct (decompose_nat n (m2 + S n)).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
    assert (m2 = x).
(* Goal: forall _ : le (knot_level_def k'') (knot_level_def k), False *)
(* Goal: le (knot_level_def k'') (knot_level_def k) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    omega.
(* Goal: @eq (option knot) (match x return (forall _ : _functor F (sinv x), option knot) with | O => fun _ : _functor F (sinv O) => @None knot | S m => fun f : _functor F (sinv (S m)) => @Some (@sigT nat F_sinv) (@existT nat F_sinv m (@fmap F (sinv (S m)) (sinv m) (sinv_age m) (sinv_unage m) f)) end _f0) match n with | O => @None knot | S n => @Some knot (@existT nat F_sinv n (@fmap F predicate (sinv n) (strat n) (unstrat n) _f)) end *)
    subst x.
    replace e with (refl_equal (m2 + S n)).
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    simpl; tauto.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    apply proof_irr.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    elimtype False; omega.
  Qed.

  Lemma stratify_unstratify : forall n p H,
    proj1_sig (stratify (unstratify n p) H n) = p.
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq (sinv n) (@proj1_sig (sinv n) (fun x : sinv n => stratifies (unstratify n p) n x) (stratify (unstratify n p) H n)) p *)
    apply stratifies_unique with (unstratify n p).
(* Goal: stratifies (unstratify n p) n (@proj1_sig (sinv n) (fun x : sinv n => stratifies (unstratify n p) n x) (stratify (unstratify n p) H n)) *)
(* Goal: stratifies (unstratify n p) n p *)
    destruct (stratify _ H n).
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    simpl; auto.
(* Goal: stratifies (unstratify n p) n p *)
    clear H.
    revert p; induction n.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    simpl; intros; auto.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
    simpl; split.

(* Goal: stratifies (unstratify (S n) p) n (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p)) *)
(* Goal: forall (k : F_sinv n) (o : other), @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) match decompose_nat n (S n) with | inleft (existT _ m Hm as s) => @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o) | inright H => T_bot end *)
    assert (stratifies (unstratify n (fst (proj1_sig p))) n (fst (proj1_sig p))).
(* Goal: stratifies (unstratify n (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p))) n (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p)) *)
(* Goal: stratifies (unstratify (S n) p) n (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p)) *)
(* Goal: forall (k : F_sinv n) (o : other), @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) match decompose_nat n (S n) with | inleft (existT _ m Hm as s) => @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o) | inright H => T_bot end *)
    apply IHn.
(* Goal: stratifies (unstratify (S n) p) n (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p)) *)
(* Goal: forall (k : F_sinv n) (o : other), @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) match decompose_nat n (S n) with | inleft (existT _ m Hm as s) => @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o) | inright H => T_bot end *)
    apply (stratifies_unstratify_more n 0 1 (fst (proj1_sig p)) p).
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    simpl; auto.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.

(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) match decompose_nat n (S n) with | inleft (existT _ m Hm as s) => @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o) | inright H => T_bot end *)
    destruct (decompose_nat n (S n)).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
(* Goal: forall _ : le (knot_level_def k'') (knot_level_def k), False *)
(* Goal: le (knot_level_def k'') (knot_level_def k) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    assert (x = 0) by omega.
(* Goal: @eq (option knot) (match x return (forall _ : _functor F (sinv x), option knot) with | O => fun _ : _functor F (sinv O) => @None knot | S m => fun f : _functor F (sinv (S m)) => @Some (@sigT nat F_sinv) (@existT nat F_sinv m (@fmap F (sinv (S m)) (sinv m) (sinv_age m) (sinv_unage m) f)) end _f0) match n with | O => @None knot | S n => @Some knot (@existT nat F_sinv n (@fmap F predicate (sinv n) (strat n) (unstrat n) _f)) end *)
    subst x.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (@eq_rect nat (S n) sinv p (S n) e)) (@pair (_functor F (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    simpl in e.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    replace e with (refl_equal (S n)) by apply proof_irr.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    split; auto.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    elimtype False; omega.
  Qed.

  Definition strat (n:nat) (p:predicate) : sinv n :=
    proj1_sig (stratify (proj1_sig p) (proj2_sig p) n).

  Definition unstrat (n:nat) (p:sinv n) : predicate :=
    exist hered (unstratify n p) (unstratify_hered n p).

  Definition squash (x:nat * F predicate) : knot :=
    match x with (n,f) => existT (F_sinv) n (fmap F (strat n) (unstrat n) f) end.

  Definition unsquash (k:knot) : nat * F predicate :=
    match k with existT _ n f => (n, fmap F (unstrat n) (strat n) f) end.

  Definition knot_level_def (k:knot) : nat :=
    fst (unsquash k).

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

  Definition knot_unage_def (k:knot) :=
    let (n,k) := unsquash k in squash (S n,k).

  Program Definition approx (n:nat) (p:predicate) : predicate :=
    fun w => if (le_gt_dec n (knot_level_def (fst w))) then T_bot else proj1_sig p w.
  Next Obligation.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    hnf; simpl; intros.
(* Goal: T_rel (if le_gt_dec n (knot_level_def k) then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    destruct (le_gt_dec n (knot_level_def k)).
(* Goal: T_rel T_bot (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    apply T_rel_bot.
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    destruct (le_gt_dec n (knot_level_def k'')).
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) T_bot *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    elimtype False.
(* Goal: False *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    cut (knot_level_def k'' <= knot_level_def k).
(* Goal: forall _ : le (knot_level_def k'') (knot_level_def k), False *)
(* Goal: le (knot_level_def k'') (knot_level_def k) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    omega.
(* Goal: le (knot_level_def k'') (knot_level_def k) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    replace (knot_level_def k'') with (knot_level_def k').
    clear -H; induction H.
(* Goal: le (knot_level_def y) (knot_level_def x) *)
(* Goal: le (knot_level_def x) (knot_level_def x) *)
(* Goal: le (knot_level_def z) (knot_level_def x) *)
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    hnf in H.
(* Goal: le (knot_level_def y) (knot_level_def x) *)
(* Goal: le (knot_level_def x) (knot_level_def x) *)
(* Goal: le (knot_level_def z) (knot_level_def x) *)
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    unfold age1_def in H.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    destruct x; destruct y; simpl.
(* Goal: le (knot_level_def (@existT nat (fun n : nat => _functor F (sinv n)) x0 _f0)) (knot_level_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f)) *)
(* Goal: le (knot_level_def x) (knot_level_def x) *)
(* Goal: le (knot_level_def z) (knot_level_def x) *)
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    destruct x; try discriminate.
(* Goal: le (knot_level_def (@existT nat (fun n : nat => _functor F (sinv n)) x0 _f0)) (knot_level_def (@existT nat (fun n : nat => _functor F (sinv n)) (S x) _f)) *)
(* Goal: le (knot_level_def x) (knot_level_def x) *)
(* Goal: le (knot_level_def z) (knot_level_def x) *)
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    inv H.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    unfold knot_level_def; simpl; auto.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    eapply le_trans; eauto.
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    inv H0.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    unfold knot_level_def; simpl; auto.

(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    destruct p as [p Hp]; simpl.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    eapply Hp; eauto.
  Qed.

  Lemma strat_unstrat : forall n,
    strat n oo unstrat n = id (sinv n).
  Proof.
(* Goal: forall n : nat, @eq (forall _ : sinv n, sinv n) (@compose (sinv n) predicate (sinv n) (strat n) (unstrat n)) (id (sinv n)) *)
    intros; extensionality p.
(* Goal: @eq (sinv n) (@compose (sinv n) predicate (sinv n) (strat n) (unstrat n) p) (id (sinv n) p) *)
    unfold compose, id.
(* Goal: @eq (sinv n) (strat n (unstrat n p)) p *)
    unfold strat, unstrat.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
(* Goal: @eq (sinv n) (@proj1_sig (sinv n) (fun x : sinv n => stratifies (unstratify n p) n x) (stratify (unstratify n p) (unstratify_hered n p) n)) p *)
    rewrite stratify_unstratify.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.
  Qed.

  Lemma predicate_eq : forall (p1 p2:predicate),
    proj1_sig p1 = proj1_sig p2 ->
    p1 = p2.
  Proof.
(* Goal: forall (p1 p2 : predicate) (_ : @eq (forall _ : prod knot other, T) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2)), @eq predicate p1 p2 *)
    intros; destruct p1; destruct p2; simpl in H.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x h) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x0 h0) *)
    subst x0.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    replace h0 with h by apply proof_irr.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.
  Qed.

  Lemma unstrat_strat : forall n,
    unstrat n oo strat n = approx n.
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq (forall _ : predicate, predicate) (@compose predicate (sinv n) predicate (unstrat n) (strat n)) (approx n) *)
    extensionality.
(* Goal: @eq (_functor F (sinv n)) (@compose (_functor F (sinv (S n))) (_functor F predicate) (_functor F (sinv n)) (@fmap F predicate (sinv n) (strat n) (unstrat n)) (@fmap F (sinv (S n)) predicate (unstrat (S n)) (strat (S n))) _f0) (@fmap F predicate (sinv n) (strat n) (unstrat n) _f) *)
    unfold compose.
(* Goal: @eq predicate (unstrat n (strat n x)) (approx n x) *)
    unfold unstrat, strat.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) hered (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n))) (unstratify_hered n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)))) (approx n x) *)
    unfold approx.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) hered (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n))) (unstratify_hered n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)))) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) (fun w : prod knot other => if le_gt_dec n (knot_level_def (@fst knot other w)) then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x w) (approx_obligation_1 n x)) *)
    apply predicate_eq.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
(* Goal: @eq (forall _ : prod knot other, T) (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n))) (fun w : prod knot other => if le_gt_dec n (knot_level_def (@fst knot other w)) then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x w) *)
    extensionality k.
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) (if le_gt_dec n (knot_level_def (@fst knot other k)) then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x k) *)
    destruct (le_gt_dec n (knot_level_def (fst k))).
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) T_bot *)
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x k) *)
    unfold unstratify.
(* Goal: @eq T (unstratify n x0 k) (x k) *)
    destruct k.
(* Goal: @eq T (unstratify n x0 k) (x k) *)
    destruct k.
(* Goal: @eq T match decompose_nat x0 n with | inleft (existT _ m Hm as s) => @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) x0)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) x0))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) x0))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) x0)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) x0) x) (floor m (S x0) (@eq_rect nat n sinv (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) (Init.Nat.add m (S x0)) Hm))) (@pair (_functor F (sinv x0)) other _f o) | inright H => T_bot end T_bot *)
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x k) *)
    unfold knot_level_def in l.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    destruct (decompose_nat x0 n); simpl.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s; simpl; elimtype False; omega.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    destruct x as [x Hx]; simpl.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    destruct (stratify x Hx n); simpl.
(* Goal: @eq T (unstratify n x0 k) (x k) *)
    destruct k.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    rewrite unstratify_Q with (Q:=x); auto.
(* Goal: lt (@projT1 nat (fun n : nat => _functor F (sinv n)) k) n *)
    unfold level in *.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    destruct k; simpl in *; auto.
  Qed.

  Lemma squash_unsquash : forall k, squash (unsquash k) = k.
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    destruct k as [n f]; simpl.
(* Goal: @eq Prop (and (@eq nat n1 n2) (KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2))) (and (@eq nat n1 n2) (KO.K0.KI.Rel KO.K0.predicate f1 f2)) *)
    f_equal.
(* Goal: @eq (_functor F (sinv n)) (@fmap F predicate (sinv n) (strat n) (unstrat n) (@fmap F (sinv n) predicate (unstrat n) (strat n) f)) f *)
    change ((fmap F (strat n) (unstrat n) oo (fmap F (unstrat n) (strat n))) f = f).
(* Goal: @eq (_functor F predicate) (@compose (_functor F predicate) (_functor F (sinv n)) (_functor F predicate) (@fmap F (sinv n) predicate (unstrat n) (strat n)) (@fmap F predicate (sinv n) (strat n) (unstrat n)) f) (@fmap F predicate predicate (approx n) (approx n) f) *)
    rewrite fmap_comp.
(* Goal: @eq (_functor F (sinv n)) (@fmap F (sinv n) (sinv n) (@compose (sinv n) predicate (sinv n) (strat n) (unstrat n)) (@compose (sinv n) predicate (sinv n) (strat n) (unstrat n)) f) f *)
    rewrite strat_unstrat.
(* Goal: @eq (_functor F (sinv n)) (@fmap F (sinv n) (sinv n) (id (sinv n)) (id (sinv n)) f) f *)
    rewrite fmap_id.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.
  Qed.

  Lemma unsquash_squash : forall n f,
    unsquash (squash (n,f)) = (n, fmap F (approx n) (approx n) f).
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq (prod nat (_functor F predicate)) (unsquash (squash (@pair nat (_functor F predicate) n f))) (@pair nat (_functor F predicate) n (@fmap F predicate predicate (approx n) (approx n) f)) *)
    unfold unsquash, squash.
(* Goal: @eq Prop (and (@eq nat n1 n2) (KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2))) (and (@eq nat n1 n2) (KO.K0.KI.Rel KO.K0.predicate f1 f2)) *)
    f_equal.
(* Goal: @eq (_functor F predicate) (@fmap F (sinv n) predicate (unstrat n) (strat n) (@fmap F predicate (sinv n) (strat n) (unstrat n) f)) (@fmap F predicate predicate (approx n) (approx n) f) *)
    change ((fmap F (unstrat n) (strat n) oo (fmap F (strat n) (unstrat n))) f = fmap F (approx n) (approx n) f).
(* Goal: @eq (_functor F predicate) (@compose (_functor F predicate) (_functor F (sinv n)) (_functor F predicate) (@fmap F (sinv n) predicate (unstrat n) (strat n)) (@fmap F predicate (sinv n) (strat n) (unstrat n)) f) (@fmap F predicate predicate (approx n) (approx n) f) *)
    rewrite fmap_comp.
(* Goal: @eq (_functor F predicate) (@fmap F predicate predicate (@compose predicate (sinv n) predicate (unstrat n) (strat n)) (@compose predicate (sinv n) predicate (unstrat n) (strat n)) f) (@fmap F predicate predicate (approx n) (approx n) f) *)
    rewrite unstrat_strat.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.
  Qed.

  Lemma strat_Sx_unstrat : forall x,
    sinv_unage x = strat (S x) oo unstrat x.
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq (forall _ : prod knot other, T) (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n))) (fun w : prod knot other => if le_gt_dec n (knot_level_def (@fst knot other w)) then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x w) *)
    extensionality k.
    unfold sinv_unage.
    generalize (sinv_unage_obligation_1); intro P.
    unfold guppy_unage.
    unfold compose, strat, unstrat.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
    apply stratifies_unique with (unstratify x k).
    revert k.
    induction x; simpl; intuition.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    destruct (decompose_nat 0 0); auto.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s; elimtype False; omega.
    eapply (stratifies_unstratify_more x 0 1).
    simpl; reflexivity.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    destruct (IHx (fst (proj1_sig k))); auto.
    destruct (decompose_nat x (S x)).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x h) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x0 h0) *)
    assert (x0 = 0) by omega; subst x0.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    replace e with (refl_equal (S x)) by apply proof_irr; auto.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    elimtype False; omega.
    destruct (decompose_nat x (S x)).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x h) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x0 h0) *)
    assert (x0 = 0) by omega; subst x0.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
    destruct (decompose_nat (S x) (S x)).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s; elimtype False; omega.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.
    destruct (decompose_nat (S x) (S x)).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s; elimtype False; omega.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.

    destruct (stratify (unstratify x k) (unstratify_hered x k) (S x)).
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    simpl stratifies in s; case s; intros.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    simpl stratifies; split; auto.
  Qed.

  Lemma strat_unstrat_Sx : forall x,
    sinv_age x = strat x oo unstrat (S x).
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq (forall _ : prod knot other, T) (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n))) (fun w : prod knot other => if le_gt_dec n (knot_level_def (@fst knot other w)) then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x w) *)
    extensionality k.
    unfold sinv_age, guppy_age.
(* Goal: @eq (_functor F (sinv n)) (@compose (_functor F (sinv (S n))) (_functor F predicate) (_functor F (sinv n)) (@fmap F predicate (sinv n) (strat n) (unstrat n)) (@fmap F (sinv (S n)) predicate (unstrat (S n)) (strat (S n))) _f0) (@fmap F predicate (sinv n) (strat n) (unstrat n) _f) *)
    unfold compose.
(* Goal: @eq (sinv n) (strat n (unstrat n p)) p *)
    unfold strat, unstrat.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
    apply stratifies_unique with (unstratify x (fst (proj1_sig k))).
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    revert k; induction x; simpl; auto.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
    split.
    eapply (stratifies_unstratify_more x 0 1 ).
    simpl; reflexivity.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
    apply IHx.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
    destruct (decompose_nat x (S x)).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x h) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x0 h0) *)
    assert (x0 = 0) by omega; subst x0.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    replace e with (refl_equal (S x)) by apply proof_irr; simpl.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    tauto.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    elimtype False; omega.
    destruct (stratify (unstratify (S x) k)
      (unstratify_hered (S x) k) x).
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    simpl; auto.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    cut (x0 = (fst (proj1_sig k))); intros.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x h) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x0 h0) *)
    subst x0.
    eapply (stratifies_unstratify_more x 1 0).
    simpl; reflexivity.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    simpl; auto.
    eapply stratifies_unique.
    apply s.
    eapply (stratifies_unstratify_more x 0 1).
    simpl; reflexivity.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
    generalize (fst (proj1_sig k) : sinv x).
(* Goal: forall _ : @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (S (Init.Nat.add m1 n)) H)))) p, @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@exist (sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) => @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) x) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    clear.
    induction x; simpl; intuition.
    eapply (stratifies_unstratify_more x 0 1).
    simpl; reflexivity.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
    apply IHx.
    destruct (decompose_nat x (S x)).
    destruct s0.
    assert (x0 = 0) by omega; subst.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    replace e with (refl_equal (S x)); simpl; auto.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    apply proof_irr.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    elimtype False; omega.
  Qed.

  Lemma age1_eq : forall k,
    age1_def k = knot_age1_def k.
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq (option knot) (age1_def k) (knot_age1_def k) *)
    unfold knot_age1_def.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    case_eq (unsquash k); intros.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    case_eq k; intros.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
(* Goal: @eq (option knot) (match x return (forall _ : _functor F (sinv x), option knot) with | O => fun _ : _functor F (sinv O) => @None knot | S m => fun f : _functor F (sinv (S m)) => @Some (@sigT nat F_sinv) (@existT nat F_sinv m (@fmap F (sinv (S m)) (sinv m) (sinv_age m) (sinv_unage m) f)) end _f0) match n with | O => @None knot | S n => @Some knot (@existT nat F_sinv n (@fmap F predicate (sinv n) (strat n) (unstrat n) _f)) end *)
    assert (n = x).
(* Goal: @eq (_functor F predicate) (@fmap F (sinv (S n)) predicate (unstrat (S n)) (strat (S n)) _f0) _f *)
    subst k.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    inv H; auto.
(* Goal: @eq (option knot) (match x return (forall _ : _functor F (sinv x), option knot) with | O => fun _ : _functor F (sinv O) => @None knot | S m => fun f : _functor F (sinv (S m)) => @Some (@sigT nat F_sinv) (@existT nat F_sinv m (@fmap F (sinv (S m)) (sinv m) (sinv_age m) (sinv_unage m) f)) end _f0) match n with | O => @None knot | S n => @Some knot (@existT nat F_sinv n (@fmap F predicate (sinv n) (strat n) (unstrat n) _f)) end *)
    subst x.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    destruct n; auto.
(* Goal: @eq Prop (and (@eq nat n1 n2) (KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2))) (and (@eq nat n1 n2) (KO.K0.KI.Rel KO.K0.predicate f1 f2)) *)
    f_equal.
(* Goal: @eq Prop (and (@eq nat n1 n2) (KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2))) (and (@eq nat n1 n2) (KO.K0.KI.Rel KO.K0.predicate f1 f2)) *)
    f_equal.

(* Goal: @eq (_functor F (sinv n)) (@fmap F (sinv (S n)) (sinv n) (sinv_age n) (sinv_unage n) _f0) (@fmap F predicate (sinv n) (strat n) (unstrat n) _f) *)
    rewrite strat_Sx_unstrat.
(* Goal: @eq (_functor F (sinv n)) (@fmap F (sinv (S n)) (sinv n) (sinv_age n) (@compose (sinv n) predicate (sinv (S n)) (strat (S n)) (unstrat n)) _f0) (@fmap F predicate (sinv n) (strat n) (unstrat n) _f) *)
    rewrite strat_unstrat_Sx.
(* Goal: @eq (_functor F (sinv n)) (@fmap F (sinv (S n)) (sinv n) (@compose (sinv (S n)) predicate (sinv n) (strat n) (unstrat (S n))) (@compose (sinv n) predicate (sinv (S n)) (strat (S n)) (unstrat n)) _f0) (@fmap F predicate (sinv n) (strat n) (unstrat n) _f) *)
    rewrite <- fmap_comp.
(* Goal: @eq (_functor F (sinv n)) (@compose (_functor F (sinv (S n))) (_functor F predicate) (_functor F (sinv n)) (@fmap F predicate (sinv n) (strat n) (unstrat n)) (@fmap F (sinv (S n)) predicate (unstrat (S n)) (strat (S n))) _f0) (@fmap F predicate (sinv n) (strat n) (unstrat n) _f) *)
    unfold compose.
(* Goal: @eq Prop (and (@eq nat n1 n2) (KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2))) (and (@eq nat n1 n2) (KO.K0.KI.Rel KO.K0.predicate f1 f2)) *)
    f_equal.
(* Goal: @eq (_functor F predicate) (@fmap F (sinv (S n)) predicate (unstrat (S n)) (strat (S n)) _f0) _f *)
    subst k.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    inv H; auto.
  Qed.

  Lemma unsquash_inj : forall k1 k2,
    unsquash k1 = unsquash k2 ->
    k1 = k2.
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq (@knot kli) k1 k2 *)
    rewrite <- (squash_unsquash k1).
(* Goal: @eq (@knot kli) (@squash kli (@unsquash kli k1)) k2 *)
    rewrite <- (squash_unsquash k2).
(* Goal: @eq (@knot kli) (@squash kli (@unsquash kli k1)) (@squash kli (@unsquash kli k2)) *)
    rewrite H.
(* Goal: @eq (@Fpred kli) (@approxF kli n Fp) Fp *)
    trivial.
  Qed.
  Arguments unsquash_inj [k1 k2] _.


  Lemma pred_ext : forall (p1 p2:predicate),
    (forall x, proj1_sig p1 x = proj1_sig p2 x) ->
    p1 = p2.
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq predicate p1 p2 *)
    destruct p1 as [p1 Hp1]; destruct p2 as [p2 Hp2].
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    assert (p1 = p2).
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    extensionality x; auto.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    subst p2.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    replace Hp2 with Hp1; auto.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    apply proof_irr.
  Qed.

  Lemma approx_spec : forall n p ko,
    proj1_sig (approx n p) ko =
     if (le_gt_dec n (knot_level_def (fst ko))) then T_bot else proj1_sig p ko.
  Proof.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    intros; simpl; auto.
  Qed.

  Lemma ag_knot_facts : ageable_facts knot knot_level_def knot_age1_def.
  Proof.
(* Goal: Output kli *)
    constructor.

    unfold knot_age1_def; unfold knot_level_def; simpl; intros x'.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    destruct (unsquash x') as [n f] eqn:?H; intros.
    destruct x' as [x f0].
    exists (squash (S x, fmap F (unstrat x) (strat x) f0)).
    rewrite unsquash_squash.
(* Goal: @eq Prop (and (@eq nat n1 n2) (KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2))) (and (@eq nat n1 n2) (KO.K0.KI.Rel KO.K0.predicate f1 f2)) *)
    f_equal. f_equal.
(* Goal: forall _ : @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (S (Init.Nat.add m1 n)) H)))) p, @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (_functor F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@exist (sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) => @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) x) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    clear.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    transitivity ((fmap F (strat x) (unstrat x) oo fmap F (approx (S x)) (approx (S x)) oo fmap F (unstrat x) (strat x)) f0); auto.
(* Goal: @eq (_functor F predicate) (@compose (_functor F predicate) (_functor F (sinv n)) (_functor F predicate) (@fmap F (sinv n) predicate (unstrat n) (strat n)) (@fmap F predicate (sinv n) (strat n) (unstrat n)) f) (@fmap F predicate predicate (approx n) (approx n) f) *)
    do 2 rewrite fmap_comp.
    rewrite compose_assoc.
    replace (strat x oo approx (S x) oo unstrat x) with (@id (sinv x)).
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    rewrite fmap_id. auto.
    rewrite <- (strat_unstrat x).
(* Goal: @eq Prop (and (@eq nat n1 n2) (KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2))) (and (@eq nat n1 n2) (KO.K0.KI.Rel KO.K0.predicate f1 f2)) *)
    f_equal.
    extensionality a.
    unfold compose, approx.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    case_eq (unstrat x a); intros.
    match goal with
      [ |- _ = exist _ ?X _ ] =>
      assert (x0 = X)
    end.
   2:{
    generalize (approx_obligation_1 (S x)
      (exist (fun p => hered p) x0 h)).
(* Goal: forall (p : @projT2 Type guppy_sig (guppy n) x) (p0 : @projT2 Type guppy_sig (guppy n) x0) (_ : forall (k : F_sinv n) (o : other), @eq T (@snd (@projT1 Type guppy_sig (guppy n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy n))) other, T) x (@pair (F_sinv n) other k o)) (Q (@pair (@sigT nat F_sinv) other (@existT nat F_sinv n k) o))) (_ : forall (k : F_sinv n) (o : other), @eq T (@snd (@projT1 Type guppy_sig (guppy n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig (guppy n))) other, T) x0 (@pair (F_sinv n) other k o)) (Q (@pair (@sigT nat F_sinv) other (@existT nat F_sinv n k) o))), @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
(* Goal: @eq (sinv_prod (@projT1 Type guppy_sig (guppy n))) x x0 *)
    rewrite <- H0.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros. f_equal. apply proof_irr.
    }
(* Goal: @eq (forall _ : predicate, predicate) (@compose predicate (sinv n) predicate (unstrat n) (strat n)) (approx n) *)
    extensionality.
    destruct x1.
    unfold unstrat in H.
(* Goal: le (knot_level_def (@existT nat (fun n : nat => _functor F (sinv n)) x0 _f0)) (knot_level_def (@existT nat (fun n : nat => _functor F (sinv n)) (S x) _f)) *)
(* Goal: le (knot_level_def x) (knot_level_def x) *)
(* Goal: le (knot_level_def z) (knot_level_def x) *)
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    inv H.
(* Goal: @eq T (unstratify n x0 k) (x k) *)
    destruct k.
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) T_bot *)
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x k) *)
    unfold unstratify.
    unfold knot_level_def.
    simpl fst.
    destruct (decompose_nat x0 x).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
    destruct (le_gt_dec (S x) x0).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    elimtype False; omega.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
    destruct (decompose_nat x0 x).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
(* Goal: forall _ : le (knot_level_def k'') (knot_level_def k), False *)
(* Goal: le (knot_level_def k'') (knot_level_def k) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    assert (x1 = x2) by omega.
    subst x2.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    replace e0 with e by apply proof_irr.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    elimtype False; omega.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    destruct (le_gt_dec (S x) x0); auto.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    destruct (decompose_nat x0 x); auto.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (_functor F (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s. elimtype False. omega.

    intro.
    unfold knot_age1_def, knot_level_def.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    case_eq (unsquash x); intros.
    destruct n; simpl; intuition;
      discriminate.

(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
    unfold knot_age1_def, knot_level_def in *.
    case_eq (unsquash x); intros; rewrite H0 in H.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    destruct n; try discriminate; simpl.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    inv H; simpl; auto.
  Qed.

  Definition ageable_knot : ageable knot :=
    mkAgeable knot knot_level_def knot_age1_def ag_knot_facts.
  Existing Instance ageable_knot.

  Definition knot_rel (k1 k2:knot) :=
    let (n,f) := unsquash k1 in
    let (n',f') := unsquash k2 in
    n = n' /\ Rel predicate f f'.

  Lemma hered_spec : forall p,
    hered p =
    (forall k k' k'' o o',
      clos_refl_trans _ age k k' ->
      knot_rel  k' k'' ->
      ORel o o' ->
      T_rel (p (k,o)) (p (k'',o'))).
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq Prop (KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2)) (KO.K0.KI.Rel KO.K0.predicate f1 f2) *)
    apply prop_ext.
    intuition.
    eapply H.
    instantiate (1:=k').
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    clear -H0; induction H0; auto.
    apply rt_step.
    unfold age_def.
    rewrite age1_eq.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    eapply rt_trans; eauto.
    destruct k' as [x f], k'' as [x0 f0].
    unfold knot_rel, unsquash in H1.
    destruct H1; subst.
(* Goal: Output kli *)
    constructor.
    apply (Rel_fmap _ _ (strat x0) (unstrat x0)) in H3.
    change f with (id _ f).
    change f0 with (id _ f0).
    rewrite <- fmap_id.
    rewrite <- (strat_unstrat x0).
(* Goal: @eq (_functor F (sinv n)) (@fmap F (sinv (S n)) (sinv n) (@compose (sinv (S n)) predicate (sinv n) (strat n) (unstrat (S n))) (@compose (sinv n) predicate (sinv (S n)) (strat (S n)) (unstrat n)) _f0) (@fmap F predicate (sinv n) (strat n) (unstrat n) _f) *)
    rewrite <- fmap_comp.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.
    assumption.

(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    hnf; intros.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    apply (H k k' k''); auto.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    clear -H0; induction H0; auto.
    apply rt_step.
    hnf.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    rewrite <- age1_eq; auto.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    eapply rt_trans; eauto.

    destruct k'; destruct k''.
    inv H1.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    hnf; split; auto.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    apply Eqdep_dec.inj_pair2_eq_dec in H5; auto.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    apply Eqdep_dec.inj_pair2_eq_dec in H7; auto.
    subst.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    apply Rel_fmap; auto.
    exact eq_nat_dec.
    exact eq_nat_dec.
  Qed.

  Lemma knot_age1 : forall k:knot,
    age1 k =
    match unsquash k with
    | (O,_) => None
    | (S n,x) => Some (squash (n,x))
    end.
  Proof.
    intros; reflexivity.
  Qed.

  Lemma knot_level : forall k:knot,
    level k = fst (unsquash k).
  Proof.
    intros; reflexivity.
  Qed.

End Knot_MixVariantHeredTOthRel.

Module KnotLemmas1.

Class Input: Type := {
  knot: Type;
  Fpred: Type;
  squash: nat * Fpred -> knot;
  unsquash: knot -> nat * Fpred;
  approxF: nat -> Fpred -> Fpred;
  squash_unsquash : forall k:knot, squash (unsquash k) = k;
  unsquash_squash : forall (n:nat) (f:Fpred),
    unsquash (squash (n,f)) = (n, approxF n f)
}.

Class Output (input: Input): Prop := {
  unsquash_inj : forall k1 k2,
    unsquash k1 = unsquash k2 ->
    k1 = k2;
  squash_surj : forall k, exists n, exists Fp,
    squash (n, Fp) = k;
  unsquash_approx : forall k n Fp,
    unsquash k = (n, Fp) ->
    Fp = approxF n Fp
}.

Lemma Proof (kli: Input): Output kli.
Proof.
(* Goal: Output kli *)
  constructor.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
  + intros.
(* Goal: @eq (@knot kli) k1 k2 *)
    rewrite <- (squash_unsquash k1).
(* Goal: @eq (@knot kli) (@squash kli (@unsquash kli k1)) k2 *)
    rewrite <- (squash_unsquash k2).
(* Goal: @eq (@knot kli) (@squash kli (@unsquash kli k1)) (@squash kli (@unsquash kli k2)) *)
    rewrite H.
(* Goal: @eq (@Fpred kli) (@approxF kli n Fp) Fp *)
    trivial.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
  + intros.
(* Goal: @ex nat (fun n : nat => @ex (@Fpred kli) (fun Fp : @Fpred kli => @eq (@knot kli) (@squash kli (@pair nat (@Fpred kli) n Fp)) k)) *)
    remember (unsquash k).
(* Goal: @ex nat (fun n : nat => @ex (@Fpred kli) (fun Fp : @Fpred kli => @eq (@knot kli) (@squash kli (@pair nat (@Fpred kli) n Fp)) k)) *)
    destruct p as [n f].
(* Goal: @ex nat (fun n : nat => @ex (@Fpred kli) (fun Fp : @Fpred kli => @eq (@knot kli) (@squash kli (@pair nat (@Fpred kli) n Fp)) k)) *)
    exists n.
(* Goal: @ex (@Fpred kli) (fun Fp : @Fpred kli => @eq (@knot kli) (@squash kli (@pair nat (@Fpred kli) n Fp)) k) *)
    exists f.
(* Goal: @eq (@knot kli) (@squash kli (@pair nat (@Fpred kli) n f)) k *)
    rewrite Heqp.
(* Goal: @eq (@knot kli) (@squash kli (@unsquash kli k)) k *)
    rewrite squash_unsquash.
(* Goal: @eq (@Fpred kli) (@approxF kli n Fp) Fp *)
    trivial.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
  + intros.
    generalize H; intro.
(* Goal: @eq (@Fpred kli) Fp (@approxF kli n Fp) *)
    rewrite <- (squash_unsquash k) in H.
(* Goal: @eq (@Fpred kli) Fp (@approxF kli n Fp) *)
    rewrite H0 in H.
(* Goal: @eq (@Fpred kli) Fp (@approxF kli n Fp) *)
    rewrite unsquash_squash in H.
(* Goal: @eq (@Fpred kli) Fp (@approxF kli n Fp) *)
    inversion H.
(* Goal: @eq (@Fpred kli) (@approxF kli n Fp) (@approxF kli n (@approxF kli n Fp)) *)
    rewrite H2.
(* Goal: @eq (@Fpred kli) Fp (@approxF kli n Fp) *)
    symmetry.
(* Goal: @eq (@Fpred kli) (@approxF kli n Fp) Fp *)
    trivial.
Qed.

End KnotLemmas1.

Module KnotLemmas2.

Class Input: Type := {
  knot: Type;
  other: Type;
  T: Type;
  t0: T;
  ageable_knot : ageable knot;
  predicate: Type;
  p2p: predicate -> (knot * other -> T);
  approx : nat -> predicate -> predicate;
  pred_ext : forall (p1 p2:predicate),
    (forall x, p2p p1 x = p2p p2 x) ->
    p1 = p2;
  approx_spec : forall n p ko,
    p2p (approx n p) ko =
     if (le_gt_dec n (level (fst ko))) then t0 else p2p p ko
}.

Class Output (input: Input): Prop := {
  approx_approx1 : forall m n,
    approx n = approx n oo approx (m+n);
  approx_approx2 : forall m n,
    approx n = approx (m+n) oo approx n
}.

Lemma Proof (kli: Input): Output kli.
Proof.
(* Goal: Output kli *)
  constructor.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
  + intros.
    extensionality p.
    apply pred_ext.
    intros [k o].
(* Goal: @eq (_functor F (sinv n)) (@compose (_functor F (sinv (S n))) (_functor F predicate) (_functor F (sinv n)) (@fmap F predicate (sinv n) (strat n) (unstrat n)) (@fmap F (sinv (S n)) predicate (unstrat (S n)) (strat (S n))) _f0) (@fmap F predicate (sinv n) (strat n) (unstrat n) _f) *)
    unfold compose.
    repeat rewrite approx_spec.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    destruct (le_gt_dec n (level k)); auto.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    destruct (le_gt_dec (m+n) (level k)); auto.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    elimtype False; omega.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
  + intros.
    extensionality p.
    apply pred_ext.
    intros [k o].
(* Goal: @eq (_functor F (sinv n)) (@compose (_functor F (sinv (S n))) (_functor F predicate) (_functor F (sinv n)) (@fmap F predicate (sinv n) (strat n) (unstrat n)) (@fmap F (sinv (S n)) predicate (unstrat (S n)) (strat (S n))) _f0) (@fmap F predicate (sinv n) (strat n) (unstrat n) _f) *)
    unfold compose.
    repeat rewrite approx_spec.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    simpl.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    destruct (le_gt_dec (m+n) (level k)); auto.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    destruct (le_gt_dec n (level k)); auto.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (_functor F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    elimtype False; omega.
Qed.

End KnotLemmas2.

Module KnotLemmas_MixVariantHeredTOthRel (K : KNOT__MIXVARIANT_HERED_T_OTH_REL).
  Import K.KI.
  Import K.

  Lemma unsquash_inj : forall k1 k2,
    unsquash k1 = unsquash k2 ->
    k1 = k2.
  Proof.
    apply
     (@KnotLemmas1.unsquash_inj
       (KnotLemmas1.Build_Input _ _ _ _ _ squash_unsquash unsquash_squash)),
     (KnotLemmas1.Proof).
  Qed.
  Arguments unsquash_inj [k1 k2] _.

  Lemma squash_surj : forall k, exists n, exists Fp,
    squash (n, Fp) = k.
  Proof.
    apply
     (@KnotLemmas1.squash_surj
       (KnotLemmas1.Build_Input _ _ _ _ _ squash_unsquash unsquash_squash)),
     (KnotLemmas1.Proof).
  Qed.

  Lemma unsquash_approx : forall k n Fp,
    unsquash k = (n, Fp) ->
    Fp = fmap F (approx n) (approx n) Fp.
  Proof.
    apply
     (@KnotLemmas1.unsquash_approx
       (KnotLemmas1.Build_Input _ _ _ _ _ squash_unsquash unsquash_squash)),
     (KnotLemmas1.Proof).
  Qed.
  Arguments unsquash_approx [k n Fp] _.

  Lemma pred_ext : forall (p1 p2:predicate),
    (forall x, proj1_sig p1 x = proj1_sig p2 x) ->
    p1 = p2.
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq predicate p1 p2 *)
    destruct p1 as [p1 Hp1]; destruct p2 as [p2 Hp2].
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    assert (p1 = p2).
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    extensionality x; auto.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    subst p2.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    replace Hp2 with Hp1; auto.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    apply proof_irr.
  Qed.

  Lemma approx_approx1 : forall m n,
    approx n = approx n oo approx (m+n).
  Proof.
    apply
     (@KnotLemmas2.approx_approx1
       (KnotLemmas2.Build_Input _ _ _ _ _ _ _ _ pred_ext approx_spec)),
     (KnotLemmas2.Proof).
  Qed.

  Lemma approx_approx2 : forall m n,
    approx n = approx (m+n) oo approx n.
  Proof.
    apply
     (@KnotLemmas2.approx_approx2
       (KnotLemmas2.Build_Input _ _ _ _ _ _ _ _ pred_ext approx_spec)),
     (KnotLemmas2.Proof).
  Qed.

End KnotLemmas_MixVariantHeredTOthRel.

Module Type KNOT_FULL_OUTPUT.
  Declare Module KI: KNOT_INPUT__MIXVARIANT_HERED_T_OTH_REL.
  Declare Module K0: KNOT__MIXVARIANT_HERED_T_OTH_REL with Module KI := KI.
  Import K0.
  Parameter predicate: Type.
  Parameter pkp: bijection predicate K0.predicate.
End KNOT_FULL_OUTPUT.

Module Type KNOT_FULL.
  Declare Module KI: KNOT_INPUT__MIXVARIANT_HERED_T_OTH_REL.
  Declare Module KO: KNOT_FULL_OUTPUT with Module KI := KI.
  Import KI.
  Import KO.

  Definition knot : Type := KO.K0.knot.
  Definition ageable_knot : ageable knot := KO.K0.ageable_knot.
  Existing Instance ageable_knot.
  Definition predicate: Type := KO.predicate.

  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 approx_spec : forall n p ko,
    proj1_sig (bij_f _ _ KO.pkp (approx n p)) ko =
     if (le_gt_dec n (level (fst ko)))
     then KI.T_bot
     else proj1_sig (bij_f _ _ KO.pkp p) ko.

  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).

  Definition knot_rel (k1 k2:knot) :=
    let (n,f) := unsquash k1 in
    let (n',f') := unsquash k2 in
    n = n' /\ KI.Rel predicate f f'.

  Axiom knot_rel_spec: forall k1 k2: knot,
    knot_rel k1 k2 = KO.K0.knot_rel k1 k2.

End KNOT_FULL.

Module Type KNOT_FULL_LEMMAS.
  Declare Module K: KNOT_FULL.
  Import K.

  Axiom unsquash_inj : forall k1 k2,
    unsquash k1 = unsquash k2 ->
    k1 = k2.
  Arguments unsquash_inj [k1 k2] _.

  Axiom squash_surj : forall k, exists n, exists Fp,
    squash (n, Fp) = k.

  Axiom unsquash_approx : forall k n Fp,
    unsquash k = (n, Fp) ->
    Fp = fmap KI.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_FULL_LEMMAS.

Module KnotFull
  (KI': KNOT_INPUT__MIXVARIANT_HERED_T_OTH_REL)
  (KO': KNOT_FULL_OUTPUT with Module KI := KI'):
  KNOT_FULL with Module KI := KI' with Module KO:=KO'.

  Import MixVariantFunctor.
  Module KI:=KI'.
  Module KO:=KO'.

  Definition knot: Type := KO.K0.knot.
  Definition ageable_knot : ageable knot := KO.K0.ageable_knot.
  Existing Instance ageable_knot.
  Definition predicate: Type := KO.predicate.

  Definition squash : (nat * KI.F predicate) -> knot :=
    fun k => KO.K0.squash
     (fst k, fmap KI.F (bij_f _ _ KO.pkp) (bij_g _ _ KO.pkp) (snd k)).

  Definition unsquash : knot -> (nat * KI.F predicate) :=
    fun k => let (n, f) := KO.K0.unsquash k in
      (n, fmap KI.F (bij_g _ _ KO.pkp) (bij_f _ _ KO.pkp) f).

  Definition approx : nat -> predicate -> predicate :=
    fun n => (bij_g _ _ KO.pkp) oo KO.K0.approx n oo (bij_f _ _ KO.pkp).

  Lemma squash_unsquash : forall k:knot, squash (unsquash k) = k.
  Proof.
    intros; unfold squash, unsquash.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    destruct (KO.K0.unsquash k) as [n f] eqn:?H; simpl.
    rewrite fmap_app, bij_fg_id, fmap_id.
    unfold id.
    rewrite <- H; apply KO.K0.squash_unsquash.
  Qed.

  Lemma unsquash_squash : forall (n:nat) (f:KI.F predicate),
    unsquash (squash (n,f)) = (n, fmap KI.F (approx n) (approx n) f).
  Proof.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    intros; unfold squash, unsquash, approx; simpl.
    rewrite KO.K0.unsquash_squash, !fmap_app, compose_assoc.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.
  Qed.

  Lemma approx_spec : forall n p ko,
    proj1_sig (bij_f _ _ KO.pkp (approx n p)) ko =
     if (le_gt_dec n (level (fst ko)))
     then KI.T_bot
     else proj1_sig (bij_f _ _ KO.pkp p) ko.
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
    rewrite <- KO.K0.approx_spec.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) hered (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n))) (unstratify_hered n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)))) (approx n x) *)
    unfold approx.
    pattern (KO.K0.approx n) at 2.
    rewrite <- (id_unit2 _ _ (KO.K0.approx n)), <- (bij_fg_id KO.pkp).
    reflexivity.
  Qed.

  Lemma knot_age1 : forall k:knot,
    age1 k =
    match unsquash k with
    | (O,_) => None
    | (S n,x) => Some (squash (n,x))
    end.
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
    unfold squash, unsquash.
    rewrite KO.K0.knot_age1.
    destruct (KO.K0.unsquash k) as [n f] eqn:?H.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    destruct n; auto.
(* Goal: @eq (option knot) (age1_def (@existT nat (fun n : nat => _functor F (sinv n)) x _f0)) match n with | O => @None knot | S n => @Some knot (squash (@pair nat (_functor F predicate) n _f)) end *)
    f_equal; simpl.
    rewrite fmap_app, bij_fg_id, fmap_id.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    auto.
  Qed.

  Lemma knot_level: forall k:knot, level k = fst (unsquash k).
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
    unfold unsquash.
    rewrite KO.K0.knot_level.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    destruct (KO.K0.unsquash k) as [n f]; auto.
  Qed.

  Definition knot_rel (k1 k2:knot) :=
    let (n,f) := unsquash k1 in
    let (n',f') := unsquash k2 in
    n = n' /\ KI.Rel predicate f f'.

  Lemma knot_rel_spec: forall k1 k2: knot,
    knot_rel k1 k2 = KO.K0.knot_rel k1 k2.
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
(* Goal: @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    unfold knot_rel, KO.K0.knot_rel, unsquash.
(* Goal: @eq Prop (let (n, f) := let (n, f) := KO.K0.unsquash k1 in @pair nat (_functor KI.F KO.predicate) n (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f) in let (n', f') := let (n0, f0) := KO.K0.unsquash k2 in @pair nat (_functor KI.F KO.predicate) n0 (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f0) in and (@eq nat n n') (KI.Rel predicate f f')) (let (n, f) := KO.K0.unsquash k1 in let (n', f') := KO.K0.unsquash k2 in and (@eq nat n n') (KO.K0.KI.Rel KO.K0.predicate f f')) *)
    destruct (KO.K0.unsquash k1) as [n1 f1].
(* Goal: @eq Prop (let (n', f') := let (n, f) := KO.K0.unsquash k2 in @pair nat (_functor KI.F KO.predicate) n (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f) in and (@eq nat n1 n') (KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) f')) (let (n', f') := KO.K0.unsquash k2 in and (@eq nat n1 n') (KO.K0.KI.Rel KO.K0.predicate f1 f')) *)
    destruct (KO.K0.unsquash k2) as [n2 f2].
(* Goal: @eq Prop (and (@eq nat n1 n2) (KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2))) (and (@eq nat n1 n2) (KO.K0.KI.Rel KO.K0.predicate f1 f2)) *)
    f_equal.
(* Goal: @eq Prop (KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2)) (KO.K0.KI.Rel KO.K0.predicate f1 f2) *)
    apply prop_ext.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    split; intros.
    + pose proof KI.Rel_fmap _ _ (bij_f _ _ KO.pkp) (bij_g _ _ KO.pkp) _ _ H.
(* Goal: KO.K0.KI.Rel KO.K0.predicate f1 f2 *)
      rewrite !fmap_app, bij_fg_id, fmap_id in H0.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
      auto.
    + pose proof KI.Rel_fmap _ _ (bij_g _ _ KO.pkp) (bij_f _ _ KO.pkp) _ _ H.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
      auto.
  Qed.

End KnotFull.

Module KnotFullLemmas (K: KNOT_FULL).
  Import K.KI.
  Import K.

  Lemma unsquash_inj : forall k1 k2,
    unsquash k1 = unsquash k2 ->
    k1 = k2.
  Proof.
    apply
     (@KnotLemmas1.unsquash_inj
       (KnotLemmas1.Build_Input _ _ _ _ _ squash_unsquash unsquash_squash)),
     (KnotLemmas1.Proof).
  Qed.
  Arguments unsquash_inj [k1 k2] _.

  Lemma squash_surj : forall k, exists n, exists Fp,
    squash (n, Fp) = k.
  Proof.
    apply
     (@KnotLemmas1.squash_surj
       (KnotLemmas1.Build_Input _ _ _ _ _ squash_unsquash unsquash_squash)),
     (KnotLemmas1.Proof).
  Qed.

  Lemma unsquash_approx : forall k n Fp,
    unsquash k = (n, Fp) ->
    Fp = fmap F (approx n) (approx n) Fp.
  Proof.
    apply
     (@KnotLemmas1.unsquash_approx
       (KnotLemmas1.Build_Input _ _ _ _ _ squash_unsquash unsquash_squash)),
     (KnotLemmas1.Proof).
  Qed.
  Arguments unsquash_approx [k n Fp] _.

  Lemma pred_ext : forall (p1 p2:predicate),
    (forall x, proj1_sig (bij_f _ _ KO.pkp p1) x =
               proj1_sig (bij_f _ _ KO.pkp p2) x) ->
    p1 = p2.
  Proof.
(* Goal: forall k1 k2 : knot, @eq Prop (knot_rel k1 k2) (KO.K0.knot_rel k1 k2) *)
    intros.
    change (p1 = p2) with (id K.KO.predicate p1 = id K.KO.predicate p2).
(* Goal: @eq (_functor F (sinv n)) (@compose (_functor F (sinv (S n))) (_functor F predicate) (_functor F (sinv n)) (@fmap F predicate (sinv n) (strat n) (unstrat n)) (@fmap F (sinv (S n)) predicate (unstrat (S n)) (strat (S n))) _f0) (@fmap F predicate (sinv n) (strat n) (unstrat n) _f) *)
    rewrite <- (bij_gf_id KO.pkp); unfold compose.
    destruct (bij_f _ _ KO.pkp p1) as [pp1 Hp1];
    destruct (bij_f _ _ KO.pkp p2) as [pp2 Hp2].
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
    assert (pp1 = pp2).
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    extensionality x; auto.
    subst pp2.
(* Goal: KI.Rel predicate (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f1) (@fmap KI.F KO.K0.predicate KO.predicate (bij_g KO.predicate KO.K0.predicate KO.pkp) (bij_f KO.predicate KO.K0.predicate KO.pkp) f2) *)
    replace Hp2 with Hp1; auto.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    apply proof_irr.
  Qed.

  Lemma approx_approx1 : forall m n,
    approx n = approx n oo approx (m+n).
  Proof.
    apply
     (@KnotLemmas2.approx_approx1
       (KnotLemmas2.Build_Input _ _ _ _ _ _
         (@proj1_sig _ _ oo bij_f _ _ K.KO.pkp) _ pred_ext approx_spec)),
     (KnotLemmas2.Proof).
  Qed.

  Lemma approx_approx2 : forall m n,
    approx n = approx (m+n) oo approx n.
  Proof.
    apply
     (@KnotLemmas2.approx_approx2
       (KnotLemmas2.Build_Input _ _ _ _ _ _
         (@proj1_sig _ _ oo bij_f _ _ K.KO.pkp) _ pred_ext approx_spec)),
     (KnotLemmas2.Proof).
  Qed.

End KnotFullLemmas.














(*
Module Type KNOT_FULL_INPUT.
  Parameter F : functor.

  Parameter other : Type.

  Parameter Rel : forall A, F A -> F A -> Prop.

  Parameter Rel_fmap : forall A B (f1: A->B) (f2:B->A) x y,
    Rel A x y ->
    Rel B (fmap F f1 f2 x) (fmap F f1 f2 y).
  Axiom Rel_refl : forall A x, Rel A x x.
  Axiom Rel_trans : forall A x y z,
    Rel A x y -> Rel A y z -> Rel A x z.

  Parameter ORel : other -> other -> Prop.
  Axiom ORel_refl : reflexive other ORel.
  Axiom ORel_trans : transitive other ORel.

  Parameter T:Type.
  Parameter T_bot:T.

  Parameter T_rel : T -> T -> Prop.
  Parameter T_rel_bot : forall x, T_rel T_bot x.
  Parameter T_rel_refl : forall x, T_rel x x.
  Parameter T_rel_trans : transitive T T_rel.

  Parameter Pred: forall K: Type, ageable K -> (K -> K -> Prop) -> Type.

  Parameter Pred2predicate: forall {K agK KRel},
    Pred K agK KRel ->
    { p: K * other -> T |
      (forall k k' k'' o o',
      clos_refl_trans _ age k k' ->
      KRel k' k'' ->
      ORel o o' ->
      T_rel (p (k,o)) (p (k'',o'))) }.

  Parameter predicate2Pred: forall {K agK} {KRel: K -> K -> Prop},
    { p: K * other -> T |
      (forall (k k' k'': K) o o',
      clos_refl_trans _ age k k' ->
      KRel k' k'' ->
      ORel o o' ->
      T_rel (p (k,o)) (p (k'',o'))) } ->
    Pred K agK KRel.

  Axiom P2p2P: forall K agK KRel (P: Pred K agK KRel),
    predicate2Pred (Pred2predicate P) = P.

  Axiom p2P2p: forall K agK KRel p,
    Pred2predicate (@predicate2Pred K agK KRel p) = p.

End KNOT_FULL_INPUT.

Module Type KNOT_FULL.
  Declare Module KI: KNOT_FULL_INPUT.
  Import KI.

  Parameter knot:Type.
  Parameter ageable_knot : ageable knot.
  Existing Instance ageable_knot.
  Parameter knot_rel: knot -> knot -> Prop.

  Definition predicate: Type := Pred knot ageable_knot knot_rel.

  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 approx_spec : forall n p ko,
    proj1_sig (Pred2predicate (approx n (predicate2Pred p))) ko =
     if (le_gt_dec n (level (fst ko))) then T_bot else proj1_sig p ko.

  Axiom knot_rel_spec: forall (k1 k2:knot),
     knot_rel k1 k2 =
    let (n,f) := unsquash k1 in
    let (n',f') := unsquash k2 in
    n = n' /\ Rel predicate f 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_FULL.

Module KnotFull (KI': KNOT_FULL_INPUT): KNOT_FULL with Module KI:=KI'.

  Import MixVariantFunctor.
  Module KI:=KI'.

  Module Input.
    Definition F: functor := KI.F.
    Definition other: Type := KI.other.
    Definition Rel: forall (A:Type), KI.F A -> KI.F A -> Prop := KI.Rel.

    Definition Rel_fmap : forall A B (f1: A->B) (f2:B->A) x y,
      Rel A x y ->
      Rel B (fmap F f1 f2 x) (fmap F f1 f2 y)
      := KI.Rel_fmap.

    Definition Rel_refl : forall A x, Rel A x x := KI.Rel_refl.

    Definition Rel_trans : forall A x y z,
      Rel A x y -> Rel A y z -> Rel A x z
      := KI.Rel_trans.

    Definition ORel := KI.ORel.
    Definition ORel_refl := KI.ORel_refl.
    Definition ORel_trans := KI.ORel_trans.

    Definition T := KI.T.
    Definition T_bot: T := KI.T_bot.
    Definition T_rel : T -> T -> Prop := KI.T_rel.
    Definition T_rel_bot : forall x, T_rel T_bot x := KI.T_rel_bot.
    Definition T_rel_refl : forall x, T_rel x x := KI.T_rel_refl.
    Definition T_rel_trans : transitive T T_rel := KI.T_rel_trans.
  End Input.

  Module K := Knot_MixVariantHeredTOthRel(Input).
  Module KL := KnotLemmas_MixVariantHeredTOthRel(K).

  Definition knot: Type := K.knot.
  Definition ageable_knot : ageable knot := K.ageable_knot.
  Existing Instance ageable_knot.
  Definition knot_rel: knot -> knot -> Prop := K.knot_rel.
  Definition predicate: Type := KI.Pred knot ageable_knot knot_rel.

  Definition squash : (nat * KI.F predicate) -> knot :=
    fun k => K.squash (fst k, fmap KI.F KI.Pred2predicate KI.predicate2Pred (snd k)).

  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 approx_spec : forall n p ko,
    proj1_sig (Pred2predicate (approx n (predicate2Pred p))) ko =
     if (le_gt_dec n (level (fst ko))) then T_bot else proj1_sig p ko.

  Axiom knot_rel_spec: forall (k1 k2:knot),
     knot_rel k1 k2 =
    let (n,f) := unsquash k1 in
    let (n',f') := unsquash k2 in
    n = n' /\ Rel predicate f 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).

*)