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

(* Knots with all the bells and whistles *)

Require Import VST.msl.base.
Require Import VST.msl.ageable.

Local Open Scope nat_scope.

Module Type TY_FUNCTOR_FULL.
  Parameter F : Type -> Type -> Type.
  Parameter bimap : forall A B C D, (A -> B) -> (C -> D) -> F B C -> F A D.
  Arguments bimap [A B C D] _ _ _.

  Axiom bimap_id : forall A B, bimap (id A) (id B) = id (F A B).
  Axiom bimap_comp : forall A B C D E F (f:B -> C) (g:A -> B) (s:F -> E) (t:E -> D),
    bimap s f oo bimap t g = bimap (t oo s) (f oo g).

  Parameter other : Type.

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

  Parameter Rel_bimap : forall A B C D (f:A->B) (s:C->D) x y,
    Rel D A x y ->
    Rel C B (bimap s f x) (bimap s f y).
  Axiom Rel_refl : forall A B x, Rel A B x x.
  Axiom Rel_trans : forall A B x y z,
    Rel A B x y -> Rel A B y z -> Rel A B x z.

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

  Parameter T:Type.
  Parameter T_bot:T.

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

End TY_FUNCTOR_FULL.

Module Type KNOT_FULL.
  Declare Module TF:TY_FUNCTOR_FULL.
  Import TF.

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

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

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

  Parameter approx : nat -> predicate -> predicate.

  Axiom squash_unsquash : forall k:knot, squash (unsquash k) = k.
  Axiom unsquash_squash : forall (n:nat) (f:F predicate predicate),
    unsquash (squash (n,f)) = (n, bimap (approx n) (approx n) f).

  Axiom approx_spec : forall n p ko,
    proj1_sig (approx n p) ko =
     if (le_gt_dec n (level (fst ko))) then T_bot else proj1_sig p ko.

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

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

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

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

End KNOT_FULL.

Module KnotFull (TF':TY_FUNCTOR_FULL) : KNOT_FULL with Module TF:=TF'.
  Module TF:=TF'.
  Import TF.

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

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

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

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

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

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

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

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

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

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

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

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

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

  Definition F_sinv n := F (sinv n) (sinv n).

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

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

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

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

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

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

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

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

    Lemma stratifies_unique : forall n p1 p2,
      stratifies n p1 ->
      stratifies n p2 ->
      p1 = p2.
    Proof.
(* Goal: forall (n : nat) (p1 p2 : sinv n) (_ : stratifies n p1) (_ : stratifies n p2), @eq (sinv n) p1 p2 *)
      induction n; simpl; intuition.
(* Goal: @eq (sinv O) p1 p2 *)
(* Goal: @eq (sinv (S n)) p1 p2 *)
      destruct p1; destruct p2; auto.
(* Goal: @eq (sinv (S n)) p1 p2 *)
      destruct p1; destruct p2.
(* Goal: @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
      simpl in *; fold guppy in *.
(* Goal: @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
      cut (x = x0).
(* Goal: None *)
      intros.
(* Goal: @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
(* Goal: @eq (sinv_prod (@projT1 Type guppy_sig (guppy n))) x x0 *)
      revert p p0 H2 H3.
(* Goal: forall (p : @projT2 Type guppy_sig (guppy n) x) (p0 : @projT2 Type guppy_sig (guppy n) x0) (_ : forall (k : F_sinv n) (o : other), @eq T (@snd (@projT1 Type guppy_sig (guppy n)) (forall _ : prod (F (@projT1 Type guppy_sig (guppy n)) (@projT1 Type guppy_sig (guppy n))) other, T) x (@pair (F_sinv n) other k o)) (Q (@pair (@sigT nat F_sinv) other (@existT nat F_sinv n k) o))) (_ : forall (k : F_sinv n) (o : other), @eq T (@snd (@projT1 Type guppy_sig (guppy n)) (forall _ : prod (F (@projT1 Type guppy_sig (guppy n)) (@projT1 Type guppy_sig (guppy n))) other, T) x0 (@pair (F_sinv n) other k o)) (Q (@pair (@sigT nat F_sinv) other (@existT nat F_sinv n k) o))), @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
(* Goal: @eq (sinv_prod (@projT1 Type guppy_sig (guppy n))) x x0 *)
      rewrite <- H0.
(* Goal: None *)
      intros.
(* Goal: @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p0) *)
(* Goal: @eq (sinv_prod (@projT1 Type guppy_sig (guppy n))) x x0 *)
      replace p0 with p by (apply proof_irr); auto.
(* Goal: @eq (sinv_prod (@projT1 Type guppy_sig (guppy n))) x x0 *)
      destruct x; destruct x0; simpl in *.
(* Goal: @eq (sinv_prod (@projT1 Type guppy_sig (guppy n))) (@pair (@projT1 Type guppy_sig (guppy n)) (forall _ : prod (F (@projT1 Type guppy_sig (guppy n)) (@projT1 Type guppy_sig (guppy n))) other, T) p1 t) (@pair (@projT1 Type guppy_sig (guppy n)) (forall _ : prod (F (@projT1 Type guppy_sig (guppy n)) (@projT1 Type guppy_sig (guppy n))) other, T) p2 t0) *)
      apply injective_projections; simpl.
(* Goal: @eq (@projT1 Type guppy_sig (guppy n)) p1 p2 *)
(* Goal: @eq (forall _ : prod (F (@projT1 Type guppy_sig (guppy n)) (@projT1 Type guppy_sig (guppy n))) other, T) t t0 *)
      apply IHn; auto.
(* Goal: None *)
      extensionality; intros.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
      simpl in *.
(* Goal: @eq T (t x) (t0 x) *)
      destruct x as [x o].
(* Goal: @eq T (t (@pair (F (@projT1 Type guppy_sig (guppy n)) (@projT1 Type guppy_sig (guppy n))) other x o)) (t0 (@pair (F (@projT1 Type guppy_sig (guppy n)) (@projT1 Type guppy_sig (guppy n))) other x o)) *)
      destruct (H2 x o); destruct (H3 x o).
(* Goal: None *)
      rewrite H2.
(* Goal: @eq T (Q (@pair (@sigT nat F_sinv) other (@existT nat F_sinv n x) o)) (t0 (@pair (F (@projT1 Type guppy_sig (guppy n)) (@projT1 Type guppy_sig (guppy n))) other x o)) *)
      rewrite H3.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
      auto.
    Qed.

    Definition stratify (n:nat) : { x:sinv n | stratifies n x }.
    Proof.
      induction n.
      exists tt; simpl; exact I.
      assert (HX:
        projT2 (guppy n)
        (proj1_sig IHn, fun v : F_sinv n * other => Q (existT F_sinv n (fst v),snd v))).
      destruct n.
(* Goal: None *)
      simpl; intros.
      eapply HQ.
      apply rt_refl.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
      constructor; auto.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
      auto.
(* Goal: None *)
      simpl; intros.
      destruct IHn; simpl.
      simpl in s; destruct s.
(* Goal: @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
      destruct x; simpl in *; fold guppy in *.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
      destruct x; simpl in *.
(* Goal: None *)
      split; hnf; simpl; intros.
      rewrite H0.
      eapply HQ.
      apply rt_step.
      hnf; simpl.
      reflexivity.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
      constructor; auto.
      unfold sinv_unage.
      replace (sinv_unage_obligation_1 n) with H1.
      unfold sinv_age.
      apply Rel_refl.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
      apply proof_irr.
      apply ORel_refl.
      eapply HQ.
      apply rt_refl.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
      constructor; auto.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
      auto.

      exists ((exist (fun x => projT2 (guppy n) x) ( proj1_sig IHn, fun v:F_sinv n * other => Q (existT (F_sinv) n (fst v),snd v) ) HX)).
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
      simpl; split; auto.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
      destruct IHn; auto.
    Qed.
  End stratifies.

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

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

  Lemma floor_shuffle:
    forall (m1 n : nat)
      (p1 : sinv (m1 + S n)) (H1 : (m1 + S n) = (S m1 + n)),
      floor (S m1) n (eq_rect (m1 + S n) sinv p1 (S m1 + n) H1) = fst (proj1_sig (floor m1 (S n) p1)).
  Proof.
(* Goal: None *)
    intros.
(* Goal: @eq (sinv n) (floor (S m1) n (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (Init.Nat.add (S m1) n) H1)) (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m1 (S n) p1))) *)
    remember (fst (proj1_sig (floor m1 (S n) p1))) as p.
(* Goal: @eq (sinv n) (floor (S m1) n (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (Init.Nat.add (S m1) n) H1)) p *)
    fold guppy in *.
(* Goal: @eq (sinv n) (floor (S m1) n (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (Init.Nat.add (S m1) n) H1)) p *)
    revert n p1 H1 p Heqp.
(* Goal: None *)
    induction m1; simpl; intros.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    replace H1 with (refl_equal (S n)) by (apply proof_irr); simpl; auto.
(* Goal: @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv p1 (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    assert (m1 + S n = S m1 + n) by omega.
(* Goal: @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
    destruct p1 as [[p1 f'] Hp1]; simpl in *; fold guppy in *.
(* Goal: @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@exist (sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) => @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) x) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    generalize (IHm1 n p1 H p Heqp).
(* Goal: forall _ : @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (S (Init.Nat.add m1 n)) H)))) p, @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@exist (sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) => @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) x) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    clear.
(* Goal: forall _ : @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (S (Init.Nat.add m1 n)) H)))) p, @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@exist (sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) => @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) x) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    revert Hp1 H1; generalize H.
(* Goal: forall (H : @eq nat (Init.Nat.add m1 (S n)) (S (Init.Nat.add m1 n))) (Hp1 : @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f')) (H1 : @eq nat (S (Init.Nat.add m1 (S n))) (S (S (Init.Nat.add m1 n)))) (_ : @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (S (Init.Nat.add m1 n)) H)))) p), @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@exist (sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) => @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) x) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    revert p1 f'.
(* Goal: @eq knot (squash (unsquash k1)) (squash (unsquash k2)) *)
    rewrite H.
(* Goal: None *)
    simpl; intros.
(* Goal: @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (S (Init.Nat.add m1 n))) sinv (@exist (sinv_prod (guppy_step_ty (guppy (Init.Nat.add m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy (Init.Nat.add m1 n))) => guppy_step_prop (guppy (Init.Nat.add m1 n)) x) (@pair (guppy_step_ty (guppy (Init.Nat.add m1 n))) (forall _ : prod (F (guppy_step_ty (guppy (Init.Nat.add m1 n))) (guppy_step_ty (guppy (Init.Nat.add m1 n)))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    replace H1 with (refl_equal (S (S (m1 + n)))) by (apply proof_irr).
(* Goal: None *)
    simpl.
(* Goal: @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) p1))) p *)
    replace H0 with (refl_equal (S (m1+n))) in H2 by (apply proof_irr).
(* Goal: @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) p1))) p *)
    simpl in H2.
(* Goal: None *)
    trivial.
  Qed.

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

(* Goal: stratifies (unstratify n p) n p *)
    clear H.
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    inv H0.
(* Goal: None *)
    simpl.
    destruct (decompose_nat n0 n); [ | apply T_rel_bot ].
(* Goal: None *)
    destruct s; simpl.
(* Goal: None *)
    destruct (floor x (S n0) (eq_rect n sinv p (x +S n0) e)); simpl.
(* Goal: None *)
    destruct n0; simpl in x0; destruct x0; simpl.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    apply p0; auto.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    apply p0; auto.
  Qed.

  Lemma unstratify_Q : forall n (p:sinv n) Q,
    stratifies Q n p ->
    forall (k:knot) (o:other),
      projT1 k < n ->
      (unstratify n p (k,o) = Q (k,o)).
  Proof.
(* Goal: None *)
    intros.
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) T_bot *)
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x k) *)
    unfold unstratify.
(* Goal: @eq T (unstratify n x0 k) (x k) *)
    destruct k.
    destruct (decompose_nat x n).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (F (sinv n) (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
    simpl in H0.
(* Goal: None *)
    2: simpl in *; elimtype False; omega.
    clear H0.
    revert p H.
    generalize e.
    rewrite e.
(* Goal: None *)
    intros.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    replace e0 with (refl_equal (x0 + S x)) by apply proof_irr.
(* Goal: None *)
    simpl.
    clear e e0.
    revert p H.
(* Goal: None *)
    induction x0; simpl; intros.
    destruct H.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.
    destruct H.
    apply IHx0.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.
  Qed.

  Lemma stratifies_unstratify_more :
    forall (n m1 m2:nat) (p1:sinv (m1+n)) (p2:sinv (m2+n)),
      floor m1 n p1 = floor m2 n p2 ->
      (stratifies (unstratify (m1+n) p1) n (floor m1 n p1) ->
       stratifies (unstratify (m2+n) p2) n (floor m2 n p2)).
  Proof.
    induction n; intuition.
    split.
(* Goal: forall _ : le (knot_level_def k'') (knot_level_def k), False *)
(* Goal: le (knot_level_def k'') (knot_level_def k) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    assert (m2 + S n = S m2 + n) by omega.
    erewrite <- floor_shuffle.
    instantiate (1:=H1).
    replace (unstratify (m2 + S n) p2)
      with (unstratify (S m2 + n) (eq_rect (m2 + S n) sinv p2 (S m2 + n) H1)).
(* Goal: @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv p1 (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    assert (m1 + S n = S m1 + n) by omega.
    eapply (IHn (S m1) (S m2)
      (eq_rect (m1 + S n) sinv p1 (S m1 + n) H2)).
    rewrite floor_shuffle.
    rewrite floor_shuffle.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    rewrite H; auto.
    clear - H0.
    rewrite floor_shuffle.
    simpl in H0.
    destruct H0.
    clear H0.
    revert p1 H.
    generalize H2.
    rewrite <- H2.
(* Goal: None *)
    intros.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    replace H0 with (refl_equal (m1 + S n)) by apply proof_irr; auto.
(* Goal: forall _ : @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (S (Init.Nat.add m1 n)) H)))) p, @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@exist (sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) => @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) x) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    clear.
    revert p2.
    generalize H1.
    rewrite H1.
(* Goal: None *)
    intros.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    replace H0 with (refl_equal (S m2 + n)) by apply proof_irr; auto.

(* Goal: None *)
    intros.
(* Goal: None *)
    simpl.
    destruct (decompose_nat n (m2 + S n)).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (F (sinv n) (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
    assert (m2 = x).
(* Goal: forall _ : le (knot_level_def k'') (knot_level_def k), False *)
(* Goal: le (knot_level_def k'') (knot_level_def k) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    omega.
(* Goal: @eq (option knot) (match x return (forall _ : F (sinv x) (sinv x), option knot) with | O => fun _ : F (sinv O) (sinv O) => @None knot | S m => fun f : F (sinv (S m)) (sinv (S m)) => @Some (@sigT nat F_sinv) (@existT nat F_sinv m (bimap (sinv m) (sinv (S m)) (sinv (S m)) (sinv m) (sinv_unage m) (sinv_age m) f)) end f0) match n with | O => @None knot | S n => @Some knot (@existT nat F_sinv n (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f)) end *)
    subst x.
    replace e with (refl_equal (m2 + S n)).
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    simpl; tauto.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    apply proof_irr.
(* Goal: None *)
    elimtype False; omega.
  Qed.

  Lemma stratify_unstratify : forall n p H,
    proj1_sig (stratify (unstratify n p) H n) = p.
  Proof.
(* Goal: None *)
    intros.
(* Goal: @eq (sinv n) (@proj1_sig (sinv n) (fun x : sinv n => stratifies (unstratify n p) n x) (stratify (unstratify n p) H n)) p *)
    apply stratifies_unique with (unstratify n p).
(* Goal: stratifies (unstratify n p) n (@proj1_sig (sinv n) (fun x : sinv n => stratifies (unstratify n p) n x) (stratify (unstratify n p) H n)) *)
(* Goal: stratifies (unstratify n p) n p *)
    destruct (stratify _ H n).
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    simpl; auto.
(* Goal: stratifies (unstratify n p) n p *)
    clear H.
    revert p; induction n.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    simpl; intros; auto.
(* Goal: None *)
    intros.
    simpl; split.

(* Goal: stratifies (unstratify (S n) p) n (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p)) *)
(* Goal: forall (k : F_sinv n) (o : other), @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) match decompose_nat n (S n) with | inleft (existT _ m Hm as s) => @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (F (sinv n) (sinv n)) other k o) | inright H => T_bot end *)
    assert (stratifies (unstratify n (fst (proj1_sig p))) n (fst (proj1_sig p))).
(* Goal: stratifies (unstratify n (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p))) n (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p)) *)
(* Goal: stratifies (unstratify (S n) p) n (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p)) *)
(* Goal: forall (k : F_sinv n) (o : other), @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) match decompose_nat n (S n) with | inleft (existT _ m Hm as s) => @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (F (sinv n) (sinv n)) other k o) | inright H => T_bot end *)
    apply IHn.
(* Goal: stratifies (unstratify (S n) p) n (@fst (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p)) *)
(* Goal: forall (k : F_sinv n) (o : other), @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) match decompose_nat n (S n) with | inleft (existT _ m Hm as s) => @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (F (sinv n) (sinv n)) other k o) | inright H => T_bot end *)
    apply (stratifies_unstratify_more n 0 1 (fst (proj1_sig p)) p).
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    simpl; auto.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.

(* Goal: None *)
    intros.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) match decompose_nat n (S n) with | inleft (existT _ m Hm as s) => @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (F (sinv n) (sinv n)) other k o) | inright H => T_bot end *)
    destruct (decompose_nat n (S n)).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (F (sinv n) (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
(* Goal: forall _ : le (knot_level_def k'') (knot_level_def k), False *)
(* Goal: le (knot_level_def k'') (knot_level_def k) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    assert (x = 0) by omega.
(* Goal: @eq (option knot) (match x return (forall _ : F (sinv x) (sinv x), option knot) with | O => fun _ : F (sinv O) (sinv O) => @None knot | S m => fun f : F (sinv (S m)) (sinv (S m)) => @Some (@sigT nat F_sinv) (@existT nat F_sinv m (bimap (sinv m) (sinv (S m)) (sinv (S m)) (sinv m) (sinv_unage m) (sinv_age m) f)) end f0) match n with | O => @None knot | S n => @Some knot (@existT nat F_sinv n (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f)) end *)
    subst x.
(* Goal: None *)
    simpl.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (@eq_rect nat (S n) sinv p (S n) e)) (@pair (F (sinv n) (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    simpl in e.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    replace e with (refl_equal (S n)) by apply proof_irr.
(* Goal: None *)
    simpl.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    split; auto.
(* Goal: None *)
    elimtype False; omega.
  Qed.

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

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

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

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

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

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

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

  Program Definition approx (n:nat) (p:predicate) : predicate :=
    fun w => if (le_gt_dec n (knot_level_def (fst w))) then T_bot else proj1_sig p w.
  Next Obligation.
(* Goal: None *)
    hnf; simpl; intros.
(* Goal: T_rel (if le_gt_dec n (knot_level_def k) then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    destruct (le_gt_dec n (knot_level_def k)).
(* Goal: T_rel T_bot (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    apply T_rel_bot.
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (if le_gt_dec n (knot_level_def k'') then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    destruct (le_gt_dec n (knot_level_def k'')).
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) T_bot *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    elimtype False.
(* Goal: False *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    cut (knot_level_def k'' <= knot_level_def k).
(* Goal: forall _ : le (knot_level_def k'') (knot_level_def k), False *)
(* Goal: le (knot_level_def k'') (knot_level_def k) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    omega.
(* Goal: le (knot_level_def k'') (knot_level_def k) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    replace (knot_level_def k'') with (knot_level_def k').
    clear -H; induction H.
(* Goal: le (knot_level_def y) (knot_level_def x) *)
(* Goal: le (knot_level_def x) (knot_level_def x) *)
(* Goal: le (knot_level_def z) (knot_level_def x) *)
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    hnf in H.
(* Goal: le (knot_level_def y) (knot_level_def x) *)
(* Goal: le (knot_level_def x) (knot_level_def x) *)
(* Goal: le (knot_level_def z) (knot_level_def x) *)
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    unfold age1_def in H.
(* Goal: None *)
    destruct x; destruct y; simpl.
(* Goal: le (knot_level_def (@existT nat (fun n : nat => F (sinv n) (sinv n)) x0 f0)) (knot_level_def (@existT nat (fun n : nat => F (sinv n) (sinv n)) x f)) *)
(* Goal: le (knot_level_def x) (knot_level_def x) *)
(* Goal: le (knot_level_def z) (knot_level_def x) *)
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    destruct x; try discriminate.
(* Goal: le (knot_level_def (@existT nat (fun n : nat => F (sinv n) (sinv n)) x0 f0)) (knot_level_def (@existT nat (fun n : nat => F (sinv n) (sinv n)) (S x) f)) *)
(* Goal: le (knot_level_def x) (knot_level_def x) *)
(* Goal: le (knot_level_def z) (knot_level_def x) *)
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    inv H.
(* Goal: None *)
    simpl.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    unfold knot_level_def; simpl; auto.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    eapply le_trans; eauto.
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    inv H0.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    unfold knot_level_def; simpl; auto.

(* Goal: None *)
    destruct p as [p Hp]; simpl.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    eapply Hp; eauto.
  Qed.

  Lemma strat_unstrat : forall n,
    strat n oo unstrat n = id (sinv n).
  Proof.
(* Goal: forall n : nat, @eq (forall _ : sinv n, sinv n) (@compose (sinv n) predicate (sinv n) (strat n) (unstrat n)) (id (sinv n)) *)
    intros; extensionality p.
(* Goal: @eq (sinv n) (@compose (sinv n) predicate (sinv n) (strat n) (unstrat n) p) (id (sinv n) p) *)
    unfold compose, id.
(* Goal: @eq (sinv n) (strat n (unstrat n p)) p *)
    unfold strat, unstrat.
(* Goal: None *)
    simpl.
(* Goal: @eq (sinv n) (@proj1_sig (sinv n) (fun x : sinv n => stratifies (unstratify n p) n x) (stratify (unstratify n p) (unstratify_hered n p) n)) p *)
    rewrite stratify_unstratify.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.
  Qed.

  Lemma predicate_eq : forall (p1 p2:predicate),
    proj1_sig p1 = proj1_sig p2 ->
    p1 = p2.
  Proof.
(* Goal: forall (p1 p2 : predicate) (_ : @eq (forall _ : prod knot other, T) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2)), @eq predicate p1 p2 *)
    intros; destruct p1; destruct p2; simpl in H.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x h) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x0 h0) *)
    subst x0.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    replace h0 with h by apply proof_irr.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.
  Qed.

  Lemma unstrat_strat : forall n,
    unstrat n oo strat n = approx n.
  Proof.
(* Goal: None *)
    intros.
(* Goal: @eq (forall _ : predicate, predicate) (@compose predicate (sinv n) predicate (unstrat n) (strat n)) (approx n) *)
    extensionality.
(* Goal: None *)
    unfold compose.
(* Goal: @eq predicate (unstrat n (strat n x)) (approx n x) *)
    unfold unstrat, strat.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) hered (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n))) (unstratify_hered n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)))) (approx n x) *)
    unfold approx.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) hered (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n))) (unstratify_hered n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)))) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) (fun w : prod knot other => if le_gt_dec n (knot_level_def (@fst knot other w)) then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x w) (approx_obligation_1 n x)) *)
    apply predicate_eq.
(* Goal: None *)
    simpl.
(* Goal: @eq (forall _ : prod knot other, T) (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n))) (fun w : prod knot other => if le_gt_dec n (knot_level_def (@fst knot other w)) then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x w) *)
    extensionality k.
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) (if le_gt_dec n (knot_level_def (@fst knot other k)) then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x k) *)
    destruct (le_gt_dec n (knot_level_def (fst k))).
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) T_bot *)
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x k) *)
    unfold unstratify.
(* Goal: @eq T (unstratify n x0 k) (x k) *)
    destruct k.
(* Goal: @eq T (unstratify n x0 k) (x k) *)
    destruct k.
(* Goal: @eq T match decompose_nat x0 n with | inleft (existT _ m Hm as s) => @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) x0)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) x0)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) x0))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) x0))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) x0)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) x0) x) (floor m (S x0) (@eq_rect nat n sinv (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) (Init.Nat.add m (S x0)) Hm))) (@pair (F (sinv x0) (sinv x0)) other f o) | inright H => T_bot end T_bot *)
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x k) *)
    unfold knot_level_def in l.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
(* Goal: None *)
    destruct (decompose_nat x0 n); simpl.
(* Goal: None *)
    destruct s; simpl; elimtype False; omega.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.
(* Goal: None *)
    destruct x as [x Hx]; simpl.
(* Goal: None *)
    destruct (stratify x Hx n); simpl.
(* Goal: @eq T (unstratify n x0 k) (x k) *)
    destruct k.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    rewrite unstratify_Q with (Q:=x); auto.
(* Goal: lt (@projT1 nat (fun n : nat => F (sinv n) (sinv n)) k) n *)
    unfold level in *.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    destruct k; simpl in *; auto.
  Qed.

  Lemma squash_unsquash : forall k, squash (unsquash k) = k.
  Proof.
(* Goal: None *)
    intros.
(* Goal: None *)
    destruct k; simpl.
(* Goal: @eq (F (sinv n) (sinv n)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) (bimap predicate (sinv (S n)) (sinv (S n)) predicate (strat (S n)) (unstrat (S n)) f0)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f) *)
    f_equal.
(* Goal: @eq (F (sinv x) (sinv x)) (bimap (sinv x) predicate predicate (sinv x) (unstrat x) (strat x) (bimap predicate (sinv x) (sinv x) predicate (strat x) (unstrat x) f)) f *)
    change ((bimap (unstrat x) (strat x) oo (bimap (strat x) (unstrat x))) f = f).
(* Goal: @eq (F predicate predicate) (@compose (F predicate predicate) (F (sinv n) (sinv n)) (F predicate predicate) (bimap predicate (sinv n) (sinv n) predicate (strat n) (unstrat n)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n)) f) (bimap predicate predicate predicate predicate (approx n) (approx n) f) *)
    rewrite bimap_comp.
(* Goal: @eq (F (sinv x) (sinv x)) (bimap (sinv x) (sinv x) (sinv x) (sinv x) (@compose (sinv x) predicate (sinv x) (strat x) (unstrat x)) (@compose (sinv x) predicate (sinv x) (strat x) (unstrat x)) f) f *)
    rewrite strat_unstrat.
(* Goal: @eq (F (sinv x) (sinv x)) (bimap (sinv x) (sinv x) (sinv x) (sinv x) (id (sinv x)) (id (sinv x)) f) f *)
    rewrite bimap_id.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.
  Qed.

  Lemma unsquash_squash : forall n f,
    unsquash (squash (n,f)) = (n, bimap (approx n) (approx n) f).
  Proof.
(* Goal: None *)
    intros.
(* Goal: @eq (prod nat (F predicate predicate)) (unsquash (squash (@pair nat (F predicate predicate) n f))) (@pair nat (F predicate predicate) n (bimap predicate predicate predicate predicate (approx n) (approx n) f)) *)
    unfold unsquash, squash.
(* Goal: @eq (F (sinv n) (sinv n)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) (bimap predicate (sinv (S n)) (sinv (S n)) predicate (strat (S n)) (unstrat (S n)) f0)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f) *)
    f_equal.
(* Goal: @eq (F predicate predicate) (bimap predicate (sinv n) (sinv n) predicate (strat n) (unstrat n) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f)) (bimap predicate predicate predicate predicate (approx n) (approx n) f) *)
    change ((bimap (strat n) (unstrat n) oo (bimap (unstrat n) (strat n))) f = bimap (approx n) (approx n) f).
(* Goal: @eq (F predicate predicate) (@compose (F predicate predicate) (F (sinv n) (sinv n)) (F predicate predicate) (bimap predicate (sinv n) (sinv n) predicate (strat n) (unstrat n)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n)) f) (bimap predicate predicate predicate predicate (approx n) (approx n) f) *)
    rewrite bimap_comp.
(* Goal: @eq (F predicate predicate) (bimap predicate predicate predicate predicate (@compose predicate (sinv n) predicate (unstrat n) (strat n)) (@compose predicate (sinv n) predicate (unstrat n) (strat n)) f) (bimap predicate predicate predicate predicate (approx n) (approx n) f) *)
    rewrite unstrat_strat.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.
  Qed.


  Lemma bimap_bimap : forall A B C X Y Z (s:X->Y) (t:Y->Z) (f:B->C) (g:A->B) x,
    bimap s f (bimap t g x) = bimap (t oo s) (f oo g) x.
  Proof.
(* Goal: None *)
    intros.
(* Goal: @eq (F (sinv n) (sinv n)) (bimap (sinv n) (sinv (S n)) (sinv (S n)) (sinv n) (@compose (sinv n) predicate (sinv (S n)) (strat (S n)) (unstrat n)) (@compose (sinv (S n)) predicate (sinv n) (strat n) (unstrat (S n))) f0) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f) *)
    rewrite <- bimap_comp.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.
  Qed.


  Lemma strat_Sx_unstrat : forall x,
    sinv_unage x = strat (S x) oo unstrat x.
  Proof.
(* Goal: None *)
    intros.
(* Goal: @eq (forall _ : prod knot other, T) (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n))) (fun w : prod knot other => if le_gt_dec n (knot_level_def (@fst knot other w)) then T_bot else @proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x w) *)
    extensionality k.
    unfold sinv_unage.
    generalize (sinv_unage_obligation_1); intro P.
    unfold guppy_unage.
    unfold compose, strat, unstrat.
(* Goal: None *)
    simpl.
    apply stratifies_unique with (unstratify x k).
    revert k.
    induction x; simpl; intuition.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    destruct (decompose_nat 0 0); auto.
(* Goal: None *)
    destruct s; elimtype False; omega.
    eapply (stratifies_unstratify_more x 0 1).
    simpl; reflexivity.
(* Goal: None *)
    simpl.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    destruct (IHx (fst (proj1_sig k))); auto.
    destruct (decompose_nat x (S x)).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (F (sinv n) (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x h) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x0 h0) *)
    assert (x0 = 0) by omega; subst x0.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    replace e with (refl_equal (S x)) by apply proof_irr; auto.
(* Goal: None *)
    elimtype False; omega.
    destruct (decompose_nat x (S x)).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (F (sinv n) (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x h) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x0 h0) *)
    assert (x0 = 0) by omega; subst x0.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
    destruct (decompose_nat (S x) (S x)).
(* Goal: None *)
    destruct s; elimtype False; omega.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.
    destruct (decompose_nat (S x) (S x)).
(* Goal: None *)
    destruct s; elimtype False; omega.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.

    destruct (stratify (unstratify x k) (unstratify_hered x k) (S x)).
(* Goal: None *)
    simpl stratifies in s; case s; intros.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    simpl stratifies; split; auto.
  Qed.

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

  Lemma age1_eq : forall k,
    age1_def k = knot_age1_def k.
  Proof.
(* Goal: None *)
    intros.
(* Goal: @eq (option knot) (age1_def k) (knot_age1_def k) *)
    unfold knot_age1_def.
(* Goal: None *)
    case_eq (unsquash k); intros.
(* Goal: None *)
    case_eq k; intros.
(* Goal: None *)
    simpl.
(* Goal: @eq (option knot) (match x return (forall _ : F (sinv x) (sinv x), option knot) with | O => fun _ : F (sinv O) (sinv O) => @None knot | S m => fun f : F (sinv (S m)) (sinv (S m)) => @Some (@sigT nat F_sinv) (@existT nat F_sinv m (bimap (sinv m) (sinv (S m)) (sinv (S m)) (sinv m) (sinv_unage m) (sinv_age m) f)) end f0) match n with | O => @None knot | S n => @Some knot (@existT nat F_sinv n (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f)) end *)
    assert (n = x).
(* Goal: @eq (F predicate predicate) (bimap predicate (sinv (S n)) (sinv (S n)) predicate (strat (S n)) (unstrat (S n)) f0) f *)
    subst k.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    inv H; auto.
(* Goal: @eq (option knot) (match x return (forall _ : F (sinv x) (sinv x), option knot) with | O => fun _ : F (sinv O) (sinv O) => @None knot | S m => fun f : F (sinv (S m)) (sinv (S m)) => @Some (@sigT nat F_sinv) (@existT nat F_sinv m (bimap (sinv m) (sinv (S m)) (sinv (S m)) (sinv m) (sinv_unage m) (sinv_age m) f)) end f0) match n with | O => @None knot | S n => @Some knot (@existT nat F_sinv n (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f)) end *)
    subst x.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    destruct n; auto.
(* Goal: @eq (F (sinv n) (sinv n)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) (bimap predicate (sinv (S n)) (sinv (S n)) predicate (strat (S n)) (unstrat (S n)) f0)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f) *)
    f_equal.
(* Goal: @eq (F (sinv n) (sinv n)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) (bimap predicate (sinv (S n)) (sinv (S n)) predicate (strat (S n)) (unstrat (S n)) f0)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f) *)
    f_equal.

(* Goal: @eq (F (sinv n) (sinv n)) (bimap (sinv n) (sinv (S n)) (sinv (S n)) (sinv n) (sinv_unage n) (sinv_age n) f0) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f) *)
    rewrite strat_Sx_unstrat.
(* Goal: @eq (F (sinv n) (sinv n)) (bimap (sinv n) (sinv (S n)) (sinv (S n)) (sinv n) (@compose (sinv n) predicate (sinv (S n)) (strat (S n)) (unstrat n)) (sinv_age n) f0) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f) *)
    rewrite strat_unstrat_Sx.
(* Goal: @eq (F (sinv n) (sinv n)) (bimap (sinv n) (sinv (S n)) (sinv (S n)) (sinv n) (@compose (sinv n) predicate (sinv (S n)) (strat (S n)) (unstrat n)) (@compose (sinv (S n)) predicate (sinv n) (strat n) (unstrat (S n))) f0) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f) *)
    rewrite <- bimap_comp.
(* Goal: None *)
    unfold compose.
(* Goal: @eq (F (sinv n) (sinv n)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) (bimap predicate (sinv (S n)) (sinv (S n)) predicate (strat (S n)) (unstrat (S n)) f0)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f) *)
    f_equal.
(* Goal: @eq (F predicate predicate) (bimap predicate (sinv (S n)) (sinv (S n)) predicate (strat (S n)) (unstrat (S n)) f0) f *)
    subst k.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    inv H; auto.
  Qed.

  Lemma unsquash_inj : forall k1 k2,
    unsquash k1 = unsquash k2 ->
    k1 = k2.
  Proof.
(* Goal: None *)
    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: None *)
    trivial.
  Qed.
  Arguments unsquash_inj [k1 k2] _.


  Lemma pred_ext : forall (p1 p2:predicate),
    (forall x, proj1_sig p1 x = proj1_sig p2 x) ->
    p1 = p2.
  Proof.
(* Goal: None *)
    intros.
(* Goal: @eq predicate p1 p2 *)
    destruct p1 as [p1 Hp1]; destruct p2 as [p2 Hp2].
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    assert (p1 = p2).
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    extensionality x; auto.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    subst p2.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    replace Hp2 with Hp1; auto.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    apply proof_irr.
  Qed.

  Lemma approx_spec : forall n p ko,
    proj1_sig (approx n p) ko =
     if (le_gt_dec n (knot_level_def (fst ko))) then T_bot else proj1_sig p ko.
  Proof.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    intros; simpl; auto.
  Qed.

  Lemma ag_knot_facts : ageable_facts knot knot_level_def knot_age1_def.
  Proof.
    constructor.

    unfold knot_age1_def; unfold knot_level_def; simpl; intros x'.
(* Goal: None *)
    case_eq (unsquash x'); intros.
    destruct x'.
    exists (squash (S x, TF'.bimap (strat x) (unstrat x) f0)).
    rewrite unsquash_squash.
(* Goal: @eq (F (sinv n) (sinv n)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) (bimap predicate (sinv (S n)) (sinv (S n)) predicate (strat (S n)) (unstrat (S n)) f0)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f) *)
    f_equal. f_equal.
(* Goal: forall _ : @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (Init.Nat.add m1 (S n)) sinv p1 (S (Init.Nat.add m1 n)) H)))) p, @eq (sinv n) (floor m1 n (@fst (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => @projT2 Type guppy_sig (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@fst (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (forall _ : prod (F (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) other, T) (@proj1_sig (sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)))) (fun x : sinv_prod (guppy_step_ty (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n))) => guppy_step_prop (guppy ((fix add (n m : nat) {struct n} : nat := match n with | O => m | S p => S (add p m) end) m1 n)) x) (@eq_rect nat (S (Init.Nat.add m1 (S n))) sinv (@exist (sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) => @projT2 Type guppy_sig (guppy (Init.Nat.add m1 (S n))) x) (@pair (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (forall _ : prod (F (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n)))) (@projT1 Type guppy_sig (guppy (Init.Nat.add m1 (S n))))) other, T) p1 f') Hp1) (S (S (Init.Nat.add m1 n))) H1)))))) p *)
    clear.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    transitivity ((TF'.bimap (unstrat x) (strat x) oo TF'.bimap (approx (S x)) (approx (S x)) oo TF'.bimap (strat x) (unstrat x)) f0); auto.
    do 2 rewrite TF'.bimap_comp.
    rewrite compose_assoc.
    replace (strat x oo approx (S x) oo unstrat x) with (@id (sinv x)).
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    rewrite TF'.bimap_id. auto.
    rewrite <- (strat_unstrat x).
(* Goal: @eq (F (sinv n) (sinv n)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) (bimap predicate (sinv (S n)) (sinv (S n)) predicate (strat (S n)) (unstrat (S n)) f0)) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f) *)
    f_equal.
    extensionality a.
    unfold compose, approx.
(* Goal: None *)
    case_eq (unstrat x a); intros.
    match goal with
      [ |- _ = exist _ ?X _ ] =>
      assert (x0 = X)
    end.
   2:{
    generalize (approx_obligation_1 (S x)
      (exist (fun p => hered p) x0 h)).
(* Goal: forall (p : @projT2 Type guppy_sig (guppy n) x) (p0 : @projT2 Type guppy_sig (guppy n) x0) (_ : forall (k : F_sinv n) (o : other), @eq T (@snd (@projT1 Type guppy_sig (guppy n)) (forall _ : prod (F (@projT1 Type guppy_sig (guppy n)) (@projT1 Type guppy_sig (guppy n))) other, T) x (@pair (F_sinv n) other k o)) (Q (@pair (@sigT nat F_sinv) other (@existT nat F_sinv n k) o))) (_ : forall (k : F_sinv n) (o : other), @eq T (@snd (@projT1 Type guppy_sig (guppy n)) (forall _ : prod (F (@projT1 Type guppy_sig (guppy n)) (@projT1 Type guppy_sig (guppy n))) other, T) x0 (@pair (F_sinv n) other k o)) (Q (@pair (@sigT nat F_sinv) other (@existT nat F_sinv n k) o))), @eq (sinv (S n)) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x p) (@exist (sinv_prod (@projT1 Type guppy_sig (guppy n))) (fun x : sinv_prod (@projT1 Type guppy_sig (guppy n)) => @projT2 Type guppy_sig (guppy n) x) x0 p0) *)
(* Goal: @eq (sinv_prod (@projT1 Type guppy_sig (guppy n))) x x0 *)
    rewrite <- H0.
(* Goal: None *)
    intros. f_equal. apply proof_irr.
   }
(* Goal: @eq (forall _ : predicate, predicate) (@compose predicate (sinv n) predicate (unstrat n) (strat n)) (approx n) *)
    extensionality.
    destruct x1.
    unfold unstrat in H.
(* Goal: le (knot_level_def (@existT nat (fun n : nat => F (sinv n) (sinv n)) x0 f0)) (knot_level_def (@existT nat (fun n : nat => F (sinv n) (sinv n)) (S x) f)) *)
(* Goal: le (knot_level_def x) (knot_level_def x) *)
(* Goal: le (knot_level_def z) (knot_level_def x) *)
(* Goal: @eq nat (knot_level_def k') (knot_level_def k'') *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    inv H.
(* Goal: @eq T (unstratify n x0 k) (x k) *)
    destruct k.
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) T_bot *)
(* Goal: @eq T (unstratify n (@proj1_sig (sinv n) (fun x0 : sinv n => stratifies (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n x0) (stratify (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) (@proj2_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x) n)) k) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) x k) *)
    unfold unstratify.
    unfold knot_level_def.
    simpl fst.
    destruct (decompose_nat x0 x).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (F (sinv n) (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
    destruct (le_gt_dec (S x) x0).
(* Goal: None *)
    elimtype False; omega.
(* Goal: None *)
    simpl.
    destruct (decompose_nat x0 x).
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (F (sinv n) (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s.
(* Goal: forall _ : le (knot_level_def k'') (knot_level_def k), False *)
(* Goal: le (knot_level_def k'') (knot_level_def k) *)
(* Goal: T_rel (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k o)) (@proj1_sig (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p (@pair knot other k'' o')) *)
    assert (x1 = x2) by omega.
    subst x2.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    replace e0 with e by apply proof_irr.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.
(* Goal: None *)
    elimtype False; omega.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    destruct (le_gt_dec (S x) x0); auto.
(* Goal: None *)
    simpl.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    destruct (decompose_nat x0 x); auto.
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) (let (m, Hm) := s in @snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) (floor m (S n) (@eq_rect nat (S n) sinv p (Init.Nat.add m (S n)) Hm))) (@pair (F (sinv n) (sinv n)) other k o)) *)
(* Goal: @eq T (@snd (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (forall _ : prod (F (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) other, T) (@proj1_sig (sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n))) (fun x : sinv_prod (@projT1 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n)) => @projT2 Type guppy_sig ((fix guppy (n : nat) : guppy_ty := match n with | O => guppy_base | S n' => guppy_step (guppy n') end) n) x) p) (@pair (F_sinv n) other k o)) T_bot *)
    destruct s. elimtype False. omega.

    intro.
    unfold knot_age1_def, knot_level_def.
(* Goal: None *)
    case_eq (unsquash x); intros.
    destruct n; simpl; intuition;
      discriminate.

(* Goal: None *)
    intros.
    unfold knot_age1_def, knot_level_def in *.
    case_eq (unsquash x); intros; rewrite H0 in H.
(* Goal: None *)
    destruct n; try discriminate; simpl.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    inv H; simpl; auto.
  Qed.

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

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

  Lemma hered_spec : forall p,
    hered p =
    (forall k k' k'' o o',
      clos_refl_trans _ age k k' ->
      knot_rel  k' k'' ->
      ORel o o' ->
      T_rel (p (k,o)) (p (k'',o'))).
  Proof.
(* Goal: None *)
    intros.
    apply prop_ext.
    intuition.
    eapply H.
    instantiate (1:=k').
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    clear -H0; induction H0; auto.
    apply rt_step.
    unfold age_def.
    rewrite age1_eq.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    eapply rt_trans; eauto.
    destruct k'; destruct k''.
    unfold knot_rel, unsquash in H1.
    destruct H1; subst.
    constructor.
    apply (Rel_bimap _ _ _ _ (strat x0) (unstrat x0)) in H3.
    change f with (id _ f).
    change f0 with (id _ f0).
    rewrite <- bimap_id.
    rewrite <- (strat_unstrat x0).
(* Goal: @eq (F (sinv n) (sinv n)) (bimap (sinv n) (sinv (S n)) (sinv (S n)) (sinv n) (@compose (sinv n) predicate (sinv (S n)) (strat (S n)) (unstrat n)) (@compose (sinv (S n)) predicate (sinv n) (strat n) (unstrat (S n))) f0) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f) *)
    rewrite <- bimap_comp.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.
    assumption.

(* Goal: None *)
    hnf; intros.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    apply (H k k' k''); auto.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    clear -H0; induction H0; auto.
    apply rt_step.
    hnf.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    rewrite <- age1_eq; auto.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    eapply rt_trans; eauto.

    destruct k'; destruct k''.
    inv H1.
(* Goal: None *)
    simpl.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    hnf; split; auto.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    apply Eqdep_dec.inj_pair2_eq_dec in H5; auto.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    apply Eqdep_dec.inj_pair2_eq_dec in H7; auto.
    subst.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    apply Rel_bimap; auto.
    exact eq_nat_dec.
    exact eq_nat_dec.
  Qed.

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

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

End KnotFull.


Module KnotFull_Lemmas (K : KNOT_FULL).
  Import K.TF.
  Import K.

  Lemma unsquash_inj : forall k1 k2,
    unsquash k1 = unsquash k2 ->
    k1 = k2.
  Proof.
(* Goal: None *)
    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: None *)
    trivial.
  Qed.
  Arguments unsquash_inj [k1 k2] _.

  Lemma squash_surj : forall k, exists n, exists Fp,
    squash (n, Fp) = k.
  Proof.
(* Goal: None *)
    intros.
(* Goal: None *)
    remember (unsquash k).
(* Goal: None *)
    destruct p.
(* Goal: None *)
    exists n.
(* Goal: None *)
    exists f.
(* Goal: None *)
    rewrite Heqp.
(* Goal: None *)
    rewrite squash_unsquash.
(* Goal: None *)
    trivial.
  Qed.

  Lemma unsquash_approx : forall k n Fp,
    unsquash k = (n, Fp) ->
    Fp = bimap (approx n) (approx n) Fp.
  Proof.
(* Goal: None *)
    intros.
    generalize H; intro.
(* Goal: None *)
    rewrite <- (squash_unsquash k) in H.
(* Goal: None *)
    rewrite H0 in H.
(* Goal: None *)
    rewrite unsquash_squash in H.
(* Goal: None *)
    inversion H.
(* Goal: None *)
    rewrite H2.
(* Goal: None *)
    symmetry.
(* Goal: None *)
    trivial.
  Qed.
  Arguments unsquash_approx [k n Fp] _.

  Lemma pred_ext : forall (p1 p2:predicate),
    (forall x, proj1_sig p1 x = proj1_sig p2 x) ->
    p1 = p2.
  Proof.
(* Goal: None *)
    intros.
(* Goal: @eq predicate p1 p2 *)
    destruct p1 as [p1 Hp1]; destruct p2 as [p2 Hp2].
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    simpl in *.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    assert (p1 = p2).
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    extensionality x; auto.
(* Goal: @eq predicate (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p1 Hp1) (@exist (forall _ : prod knot other, T) (fun p : forall _ : prod knot other, T => hered p) p2 Hp2) *)
    subst p2.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    replace Hp2 with Hp1; auto.
(* Goal: @eq (hered p1) Hp1 Hp2 *)
    apply proof_irr.
  Qed.

  Lemma approx_approx1 : forall m n,
    approx n = approx n oo approx (m+n).
  Proof.
(* Goal: None *)
    intros.
(* Goal: None *)
    extensionality p.
(* Goal: None *)
    apply pred_ext.
(* Goal: None *)
    intros [k o].
(* Goal: None *)
    unfold compose.
(* Goal: None *)
    repeat rewrite approx_spec.
(* Goal: None *)
    simpl.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    destruct (le_gt_dec n (level k)); auto.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    destruct (le_gt_dec (m+n) (level k)); auto.
(* Goal: None *)
    elimtype False; omega.
  Qed.

  Lemma approx_approx2 : forall m n,
    approx n = approx (m+n) oo approx n.
  Proof.
(* Goal: None *)
    intros.
(* Goal: None *)
    extensionality p.
(* Goal: None *)
    apply pred_ext.
(* Goal: None *)
    intros [k o].
(* Goal: None *)
    unfold compose.
(* Goal: None *)
    repeat rewrite approx_spec.
(* Goal: None *)
    simpl.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    destruct (le_gt_dec (m+n) (level k)); auto.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    destruct (le_gt_dec n (level k)); auto.
(* Goal: None *)
    elimtype False; omega.
  Qed.



  Lemma bimap_bimap : forall A B C X Y Z (s:X->Y) (t:Y->Z) (f:B->C) (g:A->B) x,
    bimap s f (bimap t g x) = bimap (t oo s) (f oo g) x.
  Proof.
(* Goal: None *)
    intros.
(* Goal: @eq (F (sinv n) (sinv n)) (bimap (sinv n) (sinv (S n)) (sinv (S n)) (sinv n) (@compose (sinv n) predicate (sinv (S n)) (strat (S n)) (unstrat n)) (@compose (sinv (S n)) predicate (sinv n) (strat n) (unstrat (S n))) f0) (bimap (sinv n) predicate predicate (sinv n) (unstrat n) (strat n) f) *)
    rewrite <- bimap_comp.
(* Goal: @eq (F X C) (bimap X Y B C s f (bimap Y Z A B t g x)) (@compose (F Z A) (F Y B) (F X C) (bimap X Y B C s f) (bimap Y Z A B t g) x) *)
    auto.
  Qed.
End KnotFull_Lemmas.
