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

Require Import VST.msl.base.
Require Import VST.msl.ageable.
Require Import Coq.Logic.Eqdep_dec.
Require Import VST.msl.functors.

Import CovariantFunctor.
Import CovariantFunctorLemmas.
Import CovariantFunctorGenerator.

Local Open Scope nat_scope.

Module Type TY_FUNCTOR.
  Parameter F : functor.

  Parameter T : Type.
  Parameter T_bot : T.

  Parameter other : Type.
End TY_FUNCTOR.

Module Type KNOT.
  Declare Module TF:TY_FUNCTOR.
  Import TF.

  Parameter knot : Type.

  Parameter ag_knot : ageable knot.
  Existing Instance ag_knot.
  Existing Instance ag_prod.

  Definition predicate := (knot * other) -> T.

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

  Definition approx (n:nat) (p:predicate) : predicate :=
     fun w => if le_gt_dec n (level w) then T_bot else p w.

  Axiom squash_unsquash : forall x, squash (unsquash x) = x.
  Axiom unsquash_squash : forall n x', unsquash (squash (n,x')) = (n,fmap F (approx n) x').


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

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

End KNOT.

Module Knot (TF':TY_FUNCTOR) : KNOT with Module TF:=TF'.
  Module TF := TF'.
  Import TF.

  (* Put the discrete pointed order on rhs *)
  Inductive leT : T -> T -> Prop :=
   | leT_refl : forall t, leT t t
   | leT_bot: forall t, leT T_bot t.

  Lemma leT_asym: forall t t',
    leT t t' -> leT t' t -> t = t'.
  Proof.
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    intros.
(* Goal: @eq T t t' *)
    inversion H; subst; auto.
(* Goal: @eq T T_bot t' *)
    inversion H0; subst; auto.
  Qed.

  Fixpoint sinv (n: nat) : Type :=
    match n with
      | O => unit
      | S n => prodT (sinv n) ((F (sinv n) * other) -> T)
    end.

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

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

  Definition predicate := knot * other -> T.

  Fixpoint stratify (n:nat) (Q:predicate) {struct n} : sinv n :=
    match n as n' return sinv n' with
    | O => tt
    | S n' => ( stratify n' Q, fun v => Q (existT (F oo sinv) n' (fst v),snd v) )
    end.

  Lemma decompose_nat : forall (x y:nat), { m:nat & y = (m + S x) } + { ge x y }.
  Proof.
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    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) : predicate := fun w =>
    match w with (existT _ nw w',e) =>
      match decompose_nat nw n with
        | inleft (existT _ m Hm) => snd (floor m (S nw) (eq_rect  n _ p (m + S nw) Hm)) (w', e)
        | inright H => T_bot
      end
    end.

  Definition proof_irr_nat := eq_proofs_unicity dec_eq_nat.
  Arguments proof_irr_nat [x] [y] _ _.

  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 (floor m1 (S n) p1).
  Proof.
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) n) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) n)) other, T) (floor m1 (S n) p1)) *)
    remember (fst (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 *)
    revert n p1 H1 p Heqp.
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    induction m1; simpl; intros.
(* Goal: @eq (sinv n) (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) n) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) n)) other, T) (@eq_rect nat (S n) sinv p1 (S n) H1)) p *)
(* Goal: @eq (sinv n) (floor m1 n (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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) (@fst (prod ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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)) (forall _ : prod (_functor F (prod ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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))) other, T) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv p1 (S (S (Init.Nat.add m1 n))) H1)))) p *)
    replace H1 with (refl_equal (S n)) by (apply proof_irr_nat); simpl; auto.
(* Goal: @eq (sinv n) (floor m1 n (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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) (@fst (prod ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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)) (forall _ : prod (_functor F (prod ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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))) other, T) (@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 n) (floor m1 n (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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) (@fst (prod ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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)) (forall _ : prod (_functor F (prod ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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))) other, T) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv p1 (S (S (Init.Nat.add m1 n))) H1)))) p *)
    destruct p1 as [p1 f'].
(* Goal: @eq (sinv n) (floor m1 n (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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) (@fst (prod ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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)) (forall _ : prod (_functor F (prod ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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))) other, T) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@pair (sinv (Init.Nat.add m1 (S n))) (forall _ : prod (_functor F (sinv (Init.Nat.add m1 (S n)))) other, T) p1 f') (S (S (Init.Nat.add m1 n))) H1)))) p *)
    generalize (IHm1 n p1 H p Heqp).
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    simpl.
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    clear.
(* Goal: forall _ : @eq (sinv n) (floor m1 n (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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) (@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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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) (@fst (prod ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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)) (forall _ : prod (_functor F (prod ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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))) other, T) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@pair (sinv (Init.Nat.add m1 (S n))) (forall _ : prod (_functor F (sinv (Init.Nat.add m1 (S n)))) other, T) p1 f') (S (S (Init.Nat.add m1 n))) H1)))) p *)
    revert H1; generalize H.
(* Goal: forall (H : @eq nat (Init.Nat.add m1 (S n)) (Init.Nat.add (S m1) n)) (H1 : @eq nat (S (Init.Nat.add m1 (S n))) (S (S (Init.Nat.add m1 n)))) (_ : @eq (sinv n) (floor m1 n (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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) (@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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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) (@fst (prod ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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)) (forall _ : prod (_functor F (prod ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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))) other, T) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@pair (sinv (Init.Nat.add m1 (S n))) (forall _ : prod (_functor F (sinv (Init.Nat.add m1 (S n)))) other, T) p1 f') (S (S (Init.Nat.add m1 n))) H1)))) p *)
    revert p1 f'.
(* Goal: @eq knot (squash (unsquash k1)) (squash (unsquash k2)) *)
    rewrite H.
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    simpl; intros.
(* Goal: @eq (sinv n) (floor m1 n (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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) (@fst (prod ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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)) (forall _ : prod (_functor F (prod ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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))) other, T) (@eq_rect nat (S (S (Init.Nat.add m1 n))) sinv (@pair (prod (sinv (Init.Nat.add m1 n)) (forall _ : prod (_functor F (sinv (Init.Nat.add m1 n))) other, T)) (forall _ : prod (_functor F (prod (sinv (Init.Nat.add m1 n)) (forall _ : prod (_functor F (sinv (Init.Nat.add m1 n))) other, T))) other, T) p1 f') (S (S (Init.Nat.add m1 n))) H1)))) p *)
    replace H1 with (refl_equal (S (S (m1 + n)))) by (apply proof_irr_nat).
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    simpl.
(* Goal: @eq (sinv n) (floor m1 n (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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) p1)) p *)
    replace H0 with (refl_equal (S (m1+n))) in H2 by (apply proof_irr_nat).
(* Goal: @eq (sinv n) (floor m1 n (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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 ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) 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) p1)) p *)
    simpl in H2.
(* Goal: @eq knot (squash (unsquash k2)) (squash (unsquash k2)) *)
    trivial.
  Qed.

  Lemma stratify_unstratify_more : forall n m1 m2 p1 p2,
    floor m1 n p1 = floor m2 n p2 ->

    (stratify n oo unstratify (m1+n)) p1 =
    (stratify n oo unstratify (m2+n)) p2.
  Proof.
    unfold compose; induction n; simpl; intros; auto.
(* Goal: @eq knot (squash (unsquash k2)) (squash (unsquash k2)) *)
    apply injective_projections; simpl; trivial.

(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    assert ((m1 + S n) =  (S m1 + n)) by omega.
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    assert ((m2 + S n) =  (S m2 + n)) by omega.
    assert (floor (S m1) n (eq_rect (m1 + S n) _ p1 _ H0) = floor (S m2) n (eq_rect (m2 + S n) _ p2 _ H1)).
    do 2 rewrite floor_shuffle.
    congruence.
    generalize (IHn (S m1) (S m2) _ _ H2).
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    clear.
    generalize H0 H1.
    revert p1 p2.
    rewrite H0; clear H0.
    rewrite H1; clear H1.
    intros p1 p2 H1 H2.
    replace H1 with (refl_equal (S m1 + n)) by (apply proof_irr_nat).
    replace H2 with (refl_equal (S m2 + n)) by (apply proof_irr_nat).
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@eq_rect nat (Init.Nat.add r (S m)) sinv (stratify (Init.Nat.add r (S m)) p) (Init.Nat.add r (S m)) (@eq_refl nat (Init.Nat.add r (S m))))) (@pair (_functor F (sinv m)) other rm e)), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot, leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    simpl; auto.

    apply extensionality; intro v.
(* Goal: forall _ : leT (p w) (unstratify (Init.Nat.add r (S m)) (stratify (Init.Nat.add r (S m)) p) w), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    unfold unstratify.
    destruct (decompose_nat n (m2 + S n)) as [[r Hr]|Hr].
    2: elimtype False; omega.
    destruct (decompose_nat n (m1 + S n)) as [[s Hs]|Hs].
    2: elimtype False; omega.
    assert (m2 = r) by omega; subst r.
    assert (m1 = s) by omega; subst s.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    simpl.
    replace Hr with (refl_equal (m2 + S n)) by (apply proof_irr_nat).
    replace Hs with (refl_equal (m1 + S n)) by (apply proof_irr_nat).
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    simpl.
    rewrite H; auto.
  Qed.

  Lemma stratify_unstratify : forall n,
         stratify n oo unstratify n = id (sinv n).
  Proof.
(* Goal: forall n : nat, @eq (forall _ : sinv n, sinv n) (@compose (sinv n) predicate (sinv n) (stratify n) (unstratify n)) (id (sinv n)) *)
    unfold id, compose; intro n; extensionality p; revert n p.
(* Goal: forall (n : nat) (p : sinv n), @eq (sinv n) (stratify n (unstratify n p)) p *)
    induction n.

(* Goal: forall p : sinv O, @eq (sinv O) (stratify O (unstratify O p)) p *)
(* Goal: forall p : sinv (S n), @eq (sinv (S n)) (stratify (S n) (unstratify (S n) p)) p *)
    intros; destruct p; auto.

(* Goal: forall p : sinv (S n), @eq (sinv (S n)) (stratify (S n) (unstratify (S n) p)) p *)
    simpl; intros [p f].
(* Goal: @eq knot (squash (unsquash k2)) (squash (unsquash k2)) *)
    apply injective_projections; simpl; trivial.

    replace (stratify n (unstratify (S n) (p,f))) with
(* Goal: @eq (_functor F (sinv n)) (id (_functor F (sinv n)) xx') xx' *)
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
            (stratify n (unstratify n p)); auto.
    replace (stratify n (unstratify n p)) with
(* Goal: @eq knot (squash (unsquash k2)) (squash (unsquash k2)) *)
      ((stratify n oo unstratify (0+n)) p) by trivial.
(* Goal: @eq knot (squash (unsquash k2)) (squash (unsquash k2)) *)
    rewrite (stratify_unstratify_more _ 0 1 p (p,f)); trivial.

(* Goal: @eq (forall _ : prod (_functor F (sinv n)) other, T) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => match decompose_nat n (S n) with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) n) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) n)) other, T) (floor m (S n) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (_functor F (sinv n)) other, T) p f) (Init.Nat.add m (S n)) Hm)) (@pair (_functor F (sinv n)) other (@fst (@compose nat Type Type (_functor F) sinv n) other v) (@snd (@compose nat Type Type (_functor F) sinv n) other v)) | inright H => T_bot end) f *)
    extensionality v.

(* Goal: @eq T match decompose_nat n (S n) with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) n) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) n)) other, T) (floor m (S n) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (_functor F (sinv n)) other, T) p f) (Init.Nat.add m (S n)) Hm)) (@pair (_functor F (sinv n)) other (@fst (@compose nat Type Type (_functor F) sinv n) other v) (@snd (@compose nat Type Type (_functor F) sinv n) other v)) | inright H => T_bot end (f v) *)
    destruct (decompose_nat n (S n)) as [[r Hr]|?]; auto.
(* Goal: @eq T (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) n) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) n)) other, T) (floor r (S n) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (_functor F (sinv n)) other, T) p f) (Init.Nat.add r (S n)) Hr)) (@pair (_functor F (sinv n)) other (@fst (@compose nat Type Type (_functor F) sinv n) other v) (@snd (@compose nat Type Type (_functor F) sinv n) other v))) (f v) *)
(* Goal: @eq T T_bot (f v) *)
    assert (r = O) by omega; subst r.
(* Goal: @eq T match decompose_nat x n with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x)) other, T) (floor m (S x) (@eq_rect nat n sinv a (Init.Nat.add m (S x)) Hm)) (@pair (_functor F (sinv x)) other _f o) | inright H => T_bot end T_bot *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    simpl in *.
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@eq_rect nat (Init.Nat.add r (S m)) sinv (stratify (Init.Nat.add r (S m)) p) (Init.Nat.add r (S m)) (@eq_refl nat (Init.Nat.add r (S m))))) (@pair (_functor F (sinv m)) other rm e)), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot, leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    replace Hr with (refl_equal (S n)) by (apply proof_irr_nat); simpl; auto.
(* Goal: @eq T (f (@pair (_functor F (sinv n)) other (@fst (@compose nat Type Type (_functor F) sinv n) other v) (@snd (@compose nat Type Type (_functor F) sinv n) other v))) (f v) *)
(* Goal: @eq T T_bot (f v) *)
    destruct v; auto.

(* Goal: @eq T (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x)) other, T) (floor x0 (S x) (@eq_rect nat n sinv a (Init.Nat.add x0 (S x)) e)) (@pair (_functor F (sinv x)) other _f o)) T_bot *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    elimtype False.
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    omega.
  Qed.

  Lemma unstratify_stratify1 : forall n (p:predicate) w,
    leT ((unstratify n oo stratify n) p w) (p w).
  Proof.
(* Goal: forall _ : leT (p w) (unstratify (Init.Nat.add r (S m)) (stratify (Init.Nat.add r (S m)) p) w), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    unfold compose; induction n; simpl; intros; unfold unstratify.

    (* 0 case *)
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    destruct w as [nw rm]; simpl.
(* Goal: leT (let (nw, w') := nw in match decompose_nat nw (S n) with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor m (S nw) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (Init.Nat.add m (S nw)) Hm)) (@pair (_functor F (sinv nw)) other w' rm) | inright H => T_bot end) (p (@pair knot other nw rm)) *)
    destruct nw as [nw e].
(* Goal: leT match decompose_nat nw O with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor m (S nw) (@eq_rect nat O sinv tt (Init.Nat.add m (S nw)) Hm)) (@pair (_functor F (sinv nw)) other e rm) | inright H => T_bot end (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)) *)
(* Goal: leT (let (k, e) := w in let (nw, w') := k in match decompose_nat nw (S n) with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor m (S nw) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (Init.Nat.add m (S nw)) Hm)) (@pair (_functor F (sinv nw)) other w' e) | inright H => T_bot end) (p w) *)
    destruct (decompose_nat nw O) as [[r Hr]|?].
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    elimtype False; omega.
(* Goal: leT T_bot (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) *)
(* Goal: @eq T T_bot (approx n p (@pair knot other a b)) *)
(* Goal: leT (approx n p (@pair knot other a b)) (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) *)
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p z) (approx n p z) *)
    apply leT_bot.

    (* S n case *)
(* Goal: leT (let (k, e) := w in let (nw, w') := k in match decompose_nat nw (S n) with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor m (S nw) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (Init.Nat.add m (S nw)) Hm)) (@pair (_functor F (sinv nw)) other w' e) | inright H => T_bot end) (p w) *)
    case_eq w; intros nw rm Hrm.
(* Goal: leT (let (nw, w') := nw in match decompose_nat nw (S n) with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor m (S nw) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (Init.Nat.add m (S nw)) Hm)) (@pair (_functor F (sinv nw)) other w' rm) | inright H => T_bot end) (p (@pair knot other nw rm)) *)
    destruct nw as [nw e].
(* Goal: leT match decompose_nat nw (S n) with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor m (S nw) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (Init.Nat.add m (S nw)) Hm)) (@pair (_functor F (sinv nw)) other e rm) | inright H => T_bot end (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)) *)
    destruct (decompose_nat nw (S n)) as [[r Hr]|?]; try (apply lt_rhs_top).
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    destruct r; simpl.

(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    assert (n = nw) by omega.
(* Goal: leT (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (S nw) Hr) (@pair (_functor F (sinv nw)) other e rm)) (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)) *)
(* Goal: leT (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor r (S nw) (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S nw))) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S nw)))) other, T) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (S (Init.Nat.add r (S nw))) Hr))) (@pair (_functor F (sinv nw)) other e rm)) (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)) *)
(* Goal: leT T_bot (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)) *)
    subst nw.
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m))) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m)))) other, T) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (S (Init.Nat.add r (S m))) Hr))) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    simpl in Hr.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    replace Hr with (refl_equal (S n)) by apply proof_irr_nat; simpl.
(* Goal: @eq (forall _ : sinv x, sinv x) (id (sinv x)) (@compose (sinv x) predicate (sinv x) (stratify x) (unstratify x)) *)
    unfold compose.
(* Goal: @eq T (unstratify n a w) (if le_gt_dec (S n) (def_knot_level (@fst knot other w)) then T_bot else unstratify n a w) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    destruct w.
(* Goal: leT (p w) (p w) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m))) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m)))) other, T) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (S (Init.Nat.add r (S m))) Hr))) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    apply leT_refl.

(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m))) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m)))) other, T) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (S (Init.Nat.add r (S m))) Hr))) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    simpl in Hr.
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    assert (n = r + S nw) by omega.
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m))) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m)))) other, T) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (S (Init.Nat.add r (S m))) Hr))) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    revert Hr; subst n.
(* Goal: forall Hr : @eq nat (S (Init.Nat.add r (S m))) (S (Init.Nat.add r (S m))), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m))) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m)))) other, T) (@eq_rect nat (S (Init.Nat.add r (S m))) sinv (@pair (sinv (Init.Nat.add r (S m))) (forall _ : prod (@compose nat Type Type (_functor F) sinv (Init.Nat.add r (S m))) other, T) (stratify (Init.Nat.add r (S m)) p) (fun v : prod (@compose nat Type Type (_functor F) sinv (Init.Nat.add r (S m))) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) (Init.Nat.add r (S m)) (@fst (@compose nat Type Type (_functor F) sinv (Init.Nat.add r (S m))) other v)) (@snd (@compose nat Type Type (_functor F) sinv (Init.Nat.add r (S m))) other v)))) (S (Init.Nat.add r (S m))) Hr))) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    intro Hr.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    replace Hr with (refl_equal (S (r+S nw))) by apply proof_irr_nat; simpl.
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    clear Hr.

(* Goal: leT (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor r (S nw) (stratify (Init.Nat.add r (S nw)) p)) (@pair (_functor F (sinv nw)) other e rm)) (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)) *)
(* Goal: leT T_bot (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)) *)
    generalize (IHn p w).
(* Goal: forall _ : leT (p w) (unstratify (Init.Nat.add r (S m)) (stratify (Init.Nat.add r (S m)) p) w), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    unfold unstratify.
(* Goal: forall _ : leT (let (k, e) := w in let (nw0, w') := k in match decompose_nat nw0 (Init.Nat.add r (S nw)) with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw0) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw0)) other, T) (floor m (S nw0) (@eq_rect nat (Init.Nat.add r (S nw)) sinv (stratify (Init.Nat.add r (S nw)) p) (Init.Nat.add m (S nw0)) Hm)) (@pair (_functor F (sinv nw0)) other w' e) | inright H => T_bot end) (p w), leT (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor r (S nw) (stratify (Init.Nat.add r (S nw)) p)) (@pair (_functor F (sinv nw)) other e rm)) (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)) *)
(* Goal: leT T_bot (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)) *)
    rewrite Hrm.
(* Goal: forall _ : leT match decompose_nat nw (Init.Nat.add r (S nw)) with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor m (S nw) (@eq_rect nat (Init.Nat.add r (S nw)) sinv (stratify (Init.Nat.add r (S nw)) p) (Init.Nat.add m (S nw)) Hm)) (@pair (_functor F (sinv nw)) other e rm) | inright H => T_bot end (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)), leT (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor r (S nw) (stratify (Init.Nat.add r (S nw)) p)) (@pair (_functor F (sinv nw)) other e rm)) (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)) *)
(* Goal: leT T_bot (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)) *)
    destruct (decompose_nat nw (r + S nw)) as [[x Hx]|?].
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor x (S m) (@eq_rect nat (Init.Nat.add r (S m)) sinv (stratify (Init.Nat.add r (S m)) p) (Init.Nat.add x (S m)) Hx)) (@pair (_functor F (sinv m)) other rm e)), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot, leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    assert (x = r) by omega; subst x.
(* Goal: forall _ : leT (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor r (S nw) (@eq_rect nat (Init.Nat.add r (S nw)) sinv (stratify (Init.Nat.add r (S nw)) p) (Init.Nat.add r (S nw)) Hx)) (@pair (_functor F (sinv nw)) other e rm)) (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)), leT (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor r (S nw) (stratify (Init.Nat.add r (S nw)) p)) (@pair (_functor F (sinv nw)) other e rm)) (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)) *)
(* Goal: forall _ : leT T_bot (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)), leT (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor r (S nw) (stratify (Init.Nat.add r (S nw)) p)) (@pair (_functor F (sinv nw)) other e rm)) (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)) *)
(* Goal: leT T_bot (p (@pair knot other (@existT nat (fun n : nat => _functor F (sinv n)) nw e) rm)) *)
    replace Hx with (refl_equal (r + S nw)) by apply proof_irr_nat.
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@eq_rect nat (Init.Nat.add r (S m)) sinv (stratify (Init.Nat.add r (S m)) p) (Init.Nat.add r (S m)) (@eq_refl nat (Init.Nat.add r (S m))))) (@pair (_functor F (sinv m)) other rm e)), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot, leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    simpl; auto.
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    elimtype False; omega.
(* Goal: leT T_bot (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) *)
(* Goal: @eq T T_bot (approx n p (@pair knot other a b)) *)
(* Goal: leT (approx n p (@pair knot other a b)) (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) *)
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p z) (approx n p z) *)
    apply leT_bot.
  Qed.

  Lemma unstratify_stratify2 : forall n p w,
     projT1 (fst w) < n ->
        leT (p w) ((unstratify n oo stratify n) p w).
  Proof.
(* Goal: @eq (forall _ : sinv x, sinv x) (id (sinv x)) (@compose (sinv x) predicate (sinv x) (stratify x) (unstratify x)) *)
    unfold compose.
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    induction n; simpl; intros.

    (* 0 case *)
(* Goal: leT (p w) (unstratify O tt w) *)
(* Goal: leT (p w) (unstratify (S n) (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) w) *)
    inversion H.

    (* S n case *)
(* Goal: forall _ : leT (p w) (unstratify (Init.Nat.add r (S m)) (stratify (Init.Nat.add r (S m)) p) w), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    unfold unstratify.
(* Goal: leT (p w) (let (k, e) := w in let (nw, w') := k in match decompose_nat nw (S n) with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor m (S nw) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (Init.Nat.add m (S nw)) Hm)) (@pair (_functor F (sinv nw)) other w' e) | inright H => T_bot end) *)
    case_eq w; intros [m rm] e Hw.
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) match decompose_nat m (S n) with | inleft (existT _ m0 Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor m0 (S m) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (Init.Nat.add m0 (S m)) Hm)) (@pair (_functor F (sinv m)) other rm e) | inright H => T_bot end *)
    assert (projT1 (fst w) = m).
(* Goal: @eq nat (@projT1 nat (fun n : nat => _functor F (sinv n)) (@fst (@sigT nat (fun n : nat => _functor F (sinv n))) other w)) m *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) match decompose_nat m (S n) with | inleft (existT _ m0 Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor m0 (S m) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (Init.Nat.add m0 (S m)) Hm)) (@pair (_functor F (sinv m)) other rm e) | inright H => T_bot end *)
    rewrite Hw; auto.

(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) match decompose_nat m (S n) with | inleft (existT _ m0 Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor m0 (S m) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (Init.Nat.add m0 (S m)) Hm)) (@pair (_functor F (sinv m)) other rm e) | inright H => T_bot end *)
    destruct (decompose_nat m (S n)) as [[r Hr]|?].
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    destruct r; simpl.

(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    assert (n = m) by omega.
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (S m) Hr) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m))) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m)))) other, T) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (S (Init.Nat.add r (S m))) Hr))) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    move H0 after H1.
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m))) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m)))) other, T) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (S (Init.Nat.add r (S m))) Hr))) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    subst m. fold sinv. simpl in Hr. rewrite (proof_irr_nat Hr (refl_equal _)). clear Hr.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    simpl.
(* Goal: @eq (forall _ : sinv x, sinv x) (id (sinv x)) (@compose (sinv x) predicate (sinv x) (stratify x) (unstratify x)) *)
    unfold compose.
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) n rm) e)) (p (@pair (@sigT nat (fun x : nat => _functor F (sinv x))) other (@existT nat (fun x : nat => _functor F (sinv x)) n rm) e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m))) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m)))) other, T) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (S (Init.Nat.add r (S m))) Hr))) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    rewrite <- Hw.
(* Goal: leT (p w) (p w) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m))) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m)))) other, T) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (S (Init.Nat.add r (S m))) Hr))) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    apply leT_refl.

(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m))) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m)))) other, T) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (S (Init.Nat.add r (S m))) Hr))) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    simpl in Hr.
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    assert (n = r + S m) by omega.
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m))) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m)))) other, T) (@eq_rect nat (S n) sinv (@pair (sinv n) (forall _ : prod (@compose nat Type Type (_functor F) sinv n) other, T) (stratify n p) (fun v : prod (@compose nat Type Type (_functor F) sinv n) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fst (@compose nat Type Type (_functor F) sinv n) other v)) (@snd (@compose nat Type Type (_functor F) sinv n) other v)))) (S (Init.Nat.add r (S m))) Hr))) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    revert Hr; subst n.
(* Goal: forall Hr : @eq nat (S (Init.Nat.add r (S m))) (S (Init.Nat.add r (S m))), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@fst ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m))) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) r (S m)))) other, T) (@eq_rect nat (S (Init.Nat.add r (S m))) sinv (@pair (sinv (Init.Nat.add r (S m))) (forall _ : prod (@compose nat Type Type (_functor F) sinv (Init.Nat.add r (S m))) other, T) (stratify (Init.Nat.add r (S m)) p) (fun v : prod (@compose nat Type Type (_functor F) sinv (Init.Nat.add r (S m))) other => p (@pair (@sigT nat (@compose nat Type Type (_functor F) sinv)) other (@existT nat (@compose nat Type Type (_functor F) sinv) (Init.Nat.add r (S m)) (@fst (@compose nat Type Type (_functor F) sinv (Init.Nat.add r (S m))) other v)) (@snd (@compose nat Type Type (_functor F) sinv (Init.Nat.add r (S m))) other v)))) (S (Init.Nat.add r (S m))) Hr))) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    intro Hr.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    replace Hr with (refl_equal (S (r+S m))) by apply proof_irr_nat; simpl.
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    clear Hr.
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    rewrite H0 in H.
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    assert (m < (r +  S m)) by omega.
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    specialize ( IHn p w).
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    rewrite H0 in IHn.
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    specialize ( IHn H1).
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    revert IHn.
(* Goal: forall _ : leT (p w) (unstratify (Init.Nat.add r (S m)) (stratify (Init.Nat.add r (S m)) p) w), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    unfold unstratify.
(* Goal: forall _ : leT (p w) (let (k, e) := w in let (nw, w') := k in match decompose_nat nw (Init.Nat.add r (S m)) with | inleft (existT _ m0 Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor m0 (S nw) (@eq_rect nat (Init.Nat.add r (S m)) sinv (stratify (Init.Nat.add r (S m)) p) (Init.Nat.add m0 (S nw)) Hm)) (@pair (_functor F (sinv nw)) other w' e) | inright H => T_bot end), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    rewrite Hw.
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) match decompose_nat m (Init.Nat.add r (S m)) with | inleft (existT _ m0 Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor m0 (S m) (@eq_rect nat (Init.Nat.add r (S m)) sinv (stratify (Init.Nat.add r (S m)) p) (Init.Nat.add m0 (S m)) Hm)) (@pair (_functor F (sinv m)) other rm e) | inright H => T_bot end, leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    destruct (decompose_nat m (r + S m)) as [[x Hx]|?].
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor x (S m) (@eq_rect nat (Init.Nat.add r (S m)) sinv (stratify (Init.Nat.add r (S m)) p) (Init.Nat.add x (S m)) Hx)) (@pair (_functor F (sinv m)) other rm e)), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot, leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    assert (x = r) by omega; subst x.
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@eq_rect nat (Init.Nat.add r (S m)) sinv (stratify (Init.Nat.add r (S m)) p) (Init.Nat.add r (S m)) Hx)) (@pair (_functor F (sinv m)) other rm e)), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot, leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    replace Hx with (refl_equal (r + S m)) by apply proof_irr_nat.
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@eq_rect nat (Init.Nat.add r (S m)) sinv (stratify (Init.Nat.add r (S m)) p) (Init.Nat.add r (S m)) (@eq_refl nat (Init.Nat.add r (S m))))) (@pair (_functor F (sinv m)) other rm e)), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot, leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    simpl; auto.
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    elimtype False; omega.
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    elimtype False; omega.
  Qed.

  Lemma unstratify_stratify3 : forall n (p:predicate) w,
    projT1 (fst w) >= n -> leT ((unstratify n oo stratify n) p w) T_bot.
  Proof.
(* Goal: forall (n : nat) (p : predicate) (w : prod (@sigT nat (fun n0 : nat => _functor F (sinv n0))) other) (_ : ge (@projT1 nat (fun n0 : nat => _functor F (sinv n0)) (@fst (@sigT nat (fun n0 : nat => _functor F (sinv n0))) other w)) n), leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p w) T_bot *)
    unfold compose, unstratify; intros n p w H.
(* Goal: leT (let (k, e) := w in let (nw, w') := k in match decompose_nat nw n with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) nw)) other, T) (floor m (S nw) (@eq_rect nat n sinv (stratify n p) (Init.Nat.add m (S nw)) Hm)) (@pair (_functor F (sinv nw)) other w' e) | inright H => T_bot end) T_bot *)
    case_eq w; intros [wn rm] e.
(* Goal: forall _ : @eq (prod (@sigT nat (fun n : nat => _functor F (sinv n))) other) w (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) wn rm) e), leT match decompose_nat wn n with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) wn) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) wn)) other, T) (floor m (S wn) (@eq_rect nat n sinv (stratify n p) (Init.Nat.add m (S wn)) Hm)) (@pair (_functor F (sinv wn)) other rm e) | inright H => T_bot end T_bot *)
    intro Hrm.
(* Goal: leT match decompose_nat wn n with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) wn) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) wn)) other, T) (floor m (S wn) (@eq_rect nat n sinv (stratify n p) (Init.Nat.add m (S wn)) Hm)) (@pair (_functor F (sinv wn)) other rm e) | inright H => T_bot end T_bot *)
    rewrite Hrm in H; simpl in H.
(* Goal: leT match decompose_nat wn n with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) wn) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) wn)) other, T) (floor m (S wn) (@eq_rect nat n sinv (stratify n p) (Init.Nat.add m (S wn)) Hm)) (@pair (_functor F (sinv wn)) other rm e) | inright H => T_bot end T_bot *)
    destruct (decompose_nat wn n) as [[r Hr]|?].
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    elimtype False; omega.
(* Goal: leT T_bot (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) *)
(* Goal: @eq T T_bot (approx n p (@pair knot other a b)) *)
(* Goal: leT (approx n p (@pair knot other a b)) (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) *)
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p z) (approx n p z) *)
    apply leT_bot.
  Qed.

  Definition squash (x:nat * F predicate) : knot :=
    match x with (n,y) => existT (F oo sinv) n (fmap F (stratify n) y) end.

  Definition unsquash (x:knot) : (nat * F predicate) :=
    match x with existT _ n y => (n, fmap F (unstratify n) y) end.

  Definition def_knot_level (k:knot) := fst (unsquash k).

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

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

  Definition approx (n:nat) (p:predicate) : predicate :=
     fun w => if le_gt_dec n (def_knot_level (fst w)) then T_bot else p w.

  Lemma squash_unsquash : forall x, squash (unsquash x) = x.
  Proof.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    intros; destruct x as [x f]; simpl.
(* Goal: @eq (forall _ : sinv x, sinv x) (id (sinv x)) (@compose (sinv x) predicate (sinv x) (stratify x) (unstratify x)) *)
    unfold compose.
    replace (fmap F (stratify x) (fmap F (unstratify x) f)) with
(* Goal: @eq knot (squash (unsquash k2)) (squash (unsquash k2)) *)
      ((fmap F (stratify x) oo fmap F (unstratify x)) f) by trivial.
(* Goal: @eq (prod nat (_functor F predicate)) (@pair nat (_functor F predicate) n (@compose (_functor F predicate) (_functor F (sinv n)) (_functor F predicate) (@fmap F (sinv n) predicate (unstratify n)) (@fmap F predicate (sinv n) (stratify n)) x')) (@pair nat (_functor F predicate) n (@fmap F predicate predicate (approx n) x')) *)
    rewrite fmap_comp.
(* Goal: @eq knot (@existT nat (fun x : nat => _functor F (sinv x)) x (@fmap F (sinv x) (sinv x) (@compose (sinv x) predicate (sinv x) (stratify x) (unstratify x)) f)) (@existT nat (fun n : nat => _functor F (sinv n)) x f) *)
    replace (stratify x oo unstratify x) with (id (sinv x)).
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@eq_rect nat (Init.Nat.add r (S m)) sinv (stratify (Init.Nat.add r (S m)) p) (Init.Nat.add r (S m)) (@eq_refl nat (Init.Nat.add r (S m))))) (@pair (_functor F (sinv m)) other rm e)), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot, leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    rewrite fmap_id; simpl; auto.
(* Goal: @eq (forall _ : sinv x, sinv x) (id (sinv x)) (@compose (sinv x) predicate (sinv x) (stratify x) (unstratify x)) *)
    unfold compose.
(* Goal: @eq (forall _ : sinv x, sinv x) (id (sinv x)) (fun x0 : sinv x => stratify x (unstratify x x0)) *)
    extensionality z.
(* Goal: @eq knot (squash (unsquash k2)) (squash (unsquash k2)) *)
    replace (stratify x (unstratify x z)) with ((stratify x oo unstratify x) z) by trivial.
(* Goal: @eq (sinv x) (id (sinv x) z) (@compose (sinv x) predicate (sinv x) (stratify x) (unstratify x) z) *)
    rewrite stratify_unstratify; auto.
  Qed.

  Lemma unsquash_squash : forall n x', unsquash (squash (n,x')) = (n,fmap F (approx n) x').
  Proof.
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    intros.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    simpl.
    replace (fmap F  (unstratify n) (fmap F (stratify n) x')) with
(* Goal: @eq knot (squash (unsquash k2)) (squash (unsquash k2)) *)
      ((fmap F (unstratify n) oo fmap F (stratify n)) x') by trivial.
(* Goal: @eq (prod nat (_functor F predicate)) (@pair nat (_functor F predicate) n (@compose (_functor F predicate) (_functor F (sinv n)) (_functor F predicate) (@fmap F (sinv n) predicate (unstratify n)) (@fmap F predicate (sinv n) (stratify n)) x')) (@pair nat (_functor F predicate) n (@fmap F predicate predicate (approx n) x')) *)
    rewrite fmap_comp.
(* Goal: @eq knot (squash (unsquash k2)) (squash (unsquash k2)) *)
    apply injective_projections; simpl; trivial.
(* Goal: @eq (_functor F predicate) (@fmap F predicate predicate (@compose predicate (sinv n) predicate (unstratify n) (stratify n)) x') (@fmap F predicate predicate (approx n) x') *)
    replace (unstratify n oo stratify n) with (approx n); auto.
(* Goal: @eq (forall _ : predicate, predicate) (approx n) (@compose predicate (sinv n) predicate (unstratify n) (stratify n)) *)
    extensionality p z.
(* Goal: @eq T (approx n p z) (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p z) *)
    apply leT_asym.

(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p z) (approx n p z) *)
    intuition.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level a) then T_bot else p (@pair knot other a b)) *)
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p z) (approx n p z) *)
    case (le_gt_dec n (def_knot_level a)); intro.
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
    replace (approx n p (a, b)) with T_bot.
(* Goal: leT T_bot (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) *)
(* Goal: @eq T T_bot (approx n p (@pair knot other a b)) *)
(* Goal: leT (approx n p (@pair knot other a b)) (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) *)
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p z) (approx n p z) *)
    apply leT_bot.
(* Goal: @eq T (p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
    unfold approx.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    simpl.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level a) then T_bot else p (@pair knot other a b)) *)
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p z) (approx n p z) *)
    case (le_gt_dec n (def_knot_level a)); intro.
(* Goal: @eq knot (squash (unsquash k2)) (squash (unsquash k2)) *)
    trivial.
(* Goal: @eq T (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x)) other, T) (floor x0 (S x) (@eq_rect nat n sinv a (Init.Nat.add x0 (S x)) e)) (@pair (_functor F (sinv x)) other _f o)) T_bot *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    elimtype False.
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    omega.
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
    replace (approx n p (a,b)) with (p (a,b)).
(* Goal: leT (p (@pair knot other a b)) (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) *)
(* Goal: @eq T (p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p z) (approx n p z) *)
    apply unstratify_stratify2.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    simpl.
(* Goal: ge (@projT1 nat (fun n : nat => _functor F (sinv n)) a) n *)
(* Goal: @eq T T_bot (approx n p (@pair knot other a b)) *)
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
    destruct a.
(* Goal: lt (@projT1 nat (fun n : nat => _functor F (sinv n)) (@existT nat (fun n : nat => _functor F (sinv n)) x _f)) n *)
(* Goal: @eq T (p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p z) (approx n p z) *)
    unfold level in g.
(* Goal: @eq T match decompose_nat x n with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x)) other, T) (floor m (S x) (@eq_rect nat n sinv a (Init.Nat.add m (S x)) Hm)) (@pair (_functor F (sinv x)) other _f o) | inright H => T_bot end T_bot *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    simpl in *.
(* Goal: @eq (_functor F (sinv n)) (id (_functor F (sinv n)) xx') xx' *)
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    auto.
(* Goal: @eq T (p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
    unfold approx.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    simpl.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level a) then T_bot else p (@pair knot other a b)) *)
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p z) (approx n p z) *)
    case (le_gt_dec n (def_knot_level a)); intro.
(* Goal: @eq T (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x)) other, T) (floor x0 (S x) (@eq_rect nat n sinv a (Init.Nat.add x0 (S x)) e)) (@pair (_functor F (sinv x)) other _f o)) T_bot *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    elimtype False.
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    omega.
(* Goal: @eq knot (squash (unsquash k2)) (squash (unsquash k2)) *)
    trivial.

(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p z) (approx n p z) *)
    intuition.
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
    destruct (le_lt_dec n (def_knot_level a)).
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
    replace (approx n p (a, b)) with T_bot.
(* Goal: @eq (_functor F (sinv n)) (id (_functor F (sinv n)) xx') xx' *)
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    apply unstratify_stratify3; auto.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    simpl.
(* Goal: ge (@projT1 nat (fun n : nat => _functor F (sinv n)) a) n *)
(* Goal: @eq T T_bot (approx n p (@pair knot other a b)) *)
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
    destruct a.
(* Goal: ge (@projT1 nat (fun n : nat => _functor F (sinv n)) (@existT nat (fun n : nat => _functor F (sinv n)) x _f)) n *)
(* Goal: @eq T T_bot (approx n p (@pair knot other a b)) *)
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
    unfold level in l.
(* Goal: @eq T match decompose_nat x n with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x)) other, T) (floor m (S x) (@eq_rect nat n sinv a (Init.Nat.add m (S x)) Hm)) (@pair (_functor F (sinv x)) other _f o) | inright H => T_bot end T_bot *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    simpl in *.
(* Goal: @eq (_functor F (sinv n)) (id (_functor F (sinv n)) xx') xx' *)
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    auto.
(* Goal: @eq T (p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
    unfold approx.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    simpl.
(* Goal: @eq (_functor F (sinv n)) (id (_functor F (sinv n)) xx') xx' *)
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    case (le_gt_dec n (def_knot_level a)); auto.
(* Goal: forall _ : le n (def_knot_level a), @eq T (p (@pair knot other a b)) T_bot *)
    intro.
(* Goal: @eq T (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x)) other, T) (floor x0 (S x) (@eq_rect nat n sinv a (Init.Nat.add x0 (S x)) e)) (@pair (_functor F (sinv x)) other _f o)) T_bot *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    elimtype False.
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    omega.
(* Goal: leT (@compose predicate (sinv n) predicate (unstratify n) (stratify n) p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
    replace (approx n p (a, b)) with (p (a, b)).
(* Goal: @eq (_functor F (sinv n)) (id (_functor F (sinv n)) xx') xx' *)
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    apply unstratify_stratify1; auto.
(* Goal: @eq T (p (@pair knot other a b)) (approx n p (@pair knot other a b)) *)
    unfold approx.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    simpl.
(* Goal: @eq (_functor F (sinv n)) (id (_functor F (sinv n)) xx') xx' *)
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    case (le_gt_dec n (def_knot_level a)); auto.
(* Goal: forall _ : le n (def_knot_level a), @eq T (p (@pair knot other a b)) T_bot *)
    intro.
(* Goal: @eq T (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x)) other, T) (floor x0 (S x) (@eq_rect nat n sinv a (Init.Nat.add x0 (S x)) e)) (@pair (_functor F (sinv x)) other _f o)) T_bot *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    elimtype False.
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    omega.
  Qed.

  Lemma unsquash_inj : forall k1 k2,
    unsquash k1 = unsquash k2 ->
    k1 = k2.
  Proof.
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    intros.
(* Goal: @eq knot k1 k2 *)
    rewrite <- (squash_unsquash k1).
(* Goal: @eq knot (squash (unsquash k1)) k2 *)
    rewrite <- (squash_unsquash k2).
(* Goal: @eq knot (squash (unsquash k1)) (squash (unsquash k2)) *)
    rewrite H.
(* Goal: @eq knot (squash (unsquash k2)) (squash (unsquash k2)) *)
    trivial.
  Qed.
  Arguments unsquash_inj [k1 k2] _.

  Lemma ag_knot_facts : ageable_facts knot def_knot_level def_knot_age1.
  Proof.
(* Goal: ageable_facts knot def_knot_level def_knot_age1 *)
    constructor.

(* Goal: forall x' : knot, @ex knot (fun x : knot => @eq (option knot) (def_knot_age1 x) (@Some knot x')) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
   unfold def_knot_age1; unfold def_knot_level; simpl; intros x'.
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    case_eq (unsquash x'); intros.
(* Goal: @eq T match decompose_nat x n with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x)) other, T) (floor m (S x) (@eq_rect nat n sinv a (Init.Nat.add m (S x)) Hm)) (@pair (_functor F (sinv x)) other _f o) | inright H => T_bot end T_bot *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    destruct x' as [n' xx']. simpl in *. inv H.
(* Goal: @ex knot (fun x : knot => @eq (option knot) (let (n0, x0) := unsquash x in match n0 with | O => @None knot | S n => @Some knot (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fmap F predicate (sinv n) (stratify n) x0)) end) (@Some knot (@existT nat (fun n : nat => _functor F (sinv n)) n xx'))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    exists (squash (S n, fmap F (unstratify n) xx')).
(* Goal: @eq (option knot) (let (n0, x) := unsquash (squash (@pair nat (_functor F predicate) (S n) (@fmap F (sinv n) predicate (unstratify n) xx'))) in match n0 with | O => @None knot | S n => @Some knot (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fmap F predicate (sinv n) (stratify n) x)) end) (@Some knot (@existT nat (fun n : nat => _functor F (sinv n)) n xx')) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    rewrite unsquash_squash.
(* Goal: @eq (forall _ : sinv n, sinv n) (@compose (sinv n) predicate (sinv n) (stratify n) (unstratify n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    f_equal.
(* Goal: @eq (forall _ : sinv n, sinv n) (@compose (sinv n) predicate (sinv n) (stratify n) (unstratify n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    f_equal.
(* Goal: @eq (_functor F (sinv n)) (id (_functor F (sinv n)) xx') xx' *)
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    transitivity ((fmap F (stratify n) oo fmap F (approx (S n)) oo fmap F (unstratify n)) xx'); auto.
(* Goal: @eq (prod nat (_functor F predicate)) (@pair nat (_functor F predicate) n (@compose (_functor F predicate) (_functor F (sinv n)) (_functor F predicate) (@fmap F (sinv n) predicate (unstratify n)) (@fmap F predicate (sinv n) (stratify n)) x')) (@pair nat (_functor F predicate) n (@fmap F predicate predicate (approx n) x')) *)
    do 2 rewrite fmap_comp.
(* Goal: @eq (_functor F (sinv n)) (@fmap F (sinv n) (sinv n) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) xx') xx' *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    replace (stratify n oo approx (S n) oo unstratify n) with (@id (sinv n)).
(* Goal: @eq (_functor F (sinv n)) (id (_functor F (sinv n)) xx') xx' *)
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    rewrite fmap_id. auto.
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
   clear.
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    rewrite <- (stratify_unstratify n).
(* Goal: @eq (forall _ : sinv n, sinv n) (@compose (sinv n) predicate (sinv n) (stratify n) (unstratify n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    f_equal. extensionality  a w.
(* Goal: @eq T (unstratify n a w) (if le_gt_dec (S n) (def_knot_level (@fst knot other w)) then T_bot else unstratify n a w) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    unfold approx, compose. destruct w.
(* Goal: @eq T (unstratify n a (@pair knot other k o)) (if le_gt_dec (S n) (def_knot_level (@fst knot other (@pair knot other k o))) then T_bot else unstratify n a (@pair knot other k o)) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    simpl fst.
(* Goal: @eq (_functor F (sinv n)) (id (_functor F (sinv n)) xx') xx' *)
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    destruct (le_gt_dec (S n) (def_knot_level k)); auto.
(* Goal: @eq T match decompose_nat x n with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x)) other, T) (floor m (S x) (@eq_rect nat n sinv a (Init.Nat.add m (S x)) Hm)) (@pair (_functor F (sinv x)) other _f o) | inright H => T_bot end T_bot *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    destruct k. simpl in *.
(* Goal: @eq T match decompose_nat x n with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x)) other, T) (floor m (S x) (@eq_rect nat n sinv a (Init.Nat.add m (S x)) Hm)) (@pair (_functor F (sinv x)) other _f o) | inright H => T_bot end T_bot *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    unfold def_knot_level in l.
(* Goal: @eq T match decompose_nat x n with | inleft (existT _ m Hm as s) => @snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x)) other, T) (floor m (S x) (@eq_rect nat n sinv a (Init.Nat.add m (S x)) Hm)) (@pair (_functor F (sinv x)) other _f o) | inright H => T_bot end T_bot *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    simpl in *.
(* Goal: @eq (_functor F (sinv n)) (id (_functor F (sinv n)) xx') xx' *)
(* Goal: @eq (forall _ : sinv n, sinv n) (id (sinv n)) (@compose (sinv n) predicate (sinv n) (stratify n) (@compose (sinv n) predicate predicate (approx (S n)) (unstratify n))) *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    destruct (decompose_nat x n); auto.
(* Goal: @eq T (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) x)) other, T) (floor x0 (S x) (@eq_rect nat n sinv a (Init.Nat.add x0 (S x)) e)) (@pair (_functor F (sinv x)) other _f o)) T_bot *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    destruct s. elimtype False.
(* Goal: False *)
(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    omega.

(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    intros.
(* Goal: iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    unfold def_knot_age1, def_knot_level.
(* Goal: @eq T (p (@pair knot other a b)) (if le_gt_dec n (def_knot_level (@fst knot other (@pair knot other a b))) then T_bot else p (@pair knot other a b)) *)
    destruct (unsquash x); simpl.
(* Goal: iff (@eq (option knot) match n with | O => @None knot | S n => @Some knot (@existT nat (@compose nat Type Type (_functor F) sinv) n (@fmap F predicate (sinv n) (stratify n) _f)) end (@None knot)) (@eq nat n O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    destruct n; intuition; try discriminate.

(* Goal: forall x : knot, iff (@eq (option knot) (def_knot_age1 x) (@None knot)) (@eq nat (def_knot_level x) O) *)
(* Goal: forall (x y : knot) (_ : @eq (option knot) (def_knot_age1 x) (@Some knot y)), @eq nat (def_knot_level x) (S (def_knot_level y)) *)
    unfold def_knot_age1, def_knot_level; intros.
(* Goal: @eq nat (@fst nat (_functor F predicate) (unsquash x)) (S (@fst nat (_functor F predicate) (unsquash y))) *)
    destruct (unsquash x).
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (@eq_rect nat (Init.Nat.add r (S m)) sinv (stratify (Init.Nat.add r (S m)) p) (Init.Nat.add r (S m)) (@eq_refl nat (Init.Nat.add r (S m))))) (@pair (_functor F (sinv m)) other rm e)), leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: forall _ : leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot, leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) (@snd ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m) (forall _ : prod (_functor F ((fix sinv (n : nat) : Type := match n with | O => unit | S n0 => prod (sinv n0) (forall _ : prod (_functor F (sinv n0)) other, T) end) m)) other, T) (floor r (S m) (stratify (Init.Nat.add r (S m)) p)) (@pair (_functor F (sinv m)) other rm e)) *)
(* Goal: leT (p (@pair (@sigT nat (fun n : nat => _functor F (sinv n))) other (@existT nat (fun n : nat => _functor F (sinv n)) m rm) e)) T_bot *)
    destruct n; inv H; simpl; auto.
  Qed.

  Definition ag_knot : ageable knot :=
    mkAgeable knot def_knot_level def_knot_age1 ag_knot_facts .
  Existing Instance ag_knot.
  Existing Instance ag_prod.


  Lemma knot_level : forall k:knot,
    level k = fst (unsquash k).
  Proof (fun k => refl_equal (def_knot_level k)).

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

End Knot.
