Translating between locally nameless and de Bruijn indices

We reason about a translation between syntax with de Bruijn indices and locally nameless variables. This consists of a function which, given a locally closed term t, outputs a term of the same shape whose leaves are de Bruijn indices and a "key": some arbitrary permutation of the names of free variables in t. Another function accepts a key and a de Bruijn term and computes a locally nameless term of the same shape. The two functions are shown to be inverses.

Table of Contents :depth: 2

Imports and setup
Operations
Theory

Imports and setup

Since we are using the Kleisli typeclass hierarchy, we import modules under the namespaces Classes.Kleisli and Theory.Kleisli.

From Tealeaves Require Export
  Backends.LN
  Backends.DB.DB
  Backends.Adapters.Key
  Classes.Kleisli.DecoratedTraversableMonad
  Functors.Option.

Import DecoratedTraversableMonad.UsefulInstances.

#[local] Generalizable Variables W T U.
#[local] Open Scope nat_scope.

Operations

Definition toLN_loc (k: key) '(depth, ix) : option LN :=
  if bound_b ix depth == true
  then
    Some (Bd ix)
  else
    map (F := option) Fr (getName k (ix - depth)).

Definition toLN
  `{Mapdt_inst: Mapdt nat T} (k: key): T nat -> option (T LN) :=
  mapdt (G := option) (toLN_loc k).

Theory

Section theory.

  Context
    `{Return_T: Return T}
    `{Map_T: Map T}
    `{Bind_TT: Bind T T}
    `{Traverse_T: Traverse T}
    `{Mapd_T: Mapd nat T}
    `{Bindt_TT: Bindt T T}
    `{Bindd_T: Bindd nat T T}
    `{Mapdt_T: Mapdt nat T}
    `{Binddt_TT: Binddt nat T T}
    `{! Compat_Map_Binddt nat T T}
    `{! Compat_Bind_Binddt nat T T}
    `{! Compat_Traverse_Binddt nat T T}
    `{! Compat_Mapd_Binddt nat T T}
    `{! Compat_Bindt_Binddt nat T T}
    `{! Compat_Bindd_Binddt nat T T}
    `{! Compat_Mapdt_Binddt nat T T}.

  Context
    `{Monad_inst: ! DecoratedTraversableMonad nat T}.

  Context
    `{Map_U: Map U}
    `{Bind_TU: Bind T U}
    `{Traverse_U: Traverse U}
    `{Mapd_U: Mapd nat U}
    `{Bindt_TU: Bindt T U}
    `{Bindd_TU: Bindd nat T U}
    `{Mapdt_U: Mapdt nat U}
    `{Binddt_TU: Binddt nat T U}
    `{! Compat_Map_Binddt nat T U}
    `{! Compat_Bind_Binddt nat T U}
    `{! Compat_Traverse_Binddt nat T U}
    `{! Compat_Mapd_Binddt nat T U}
    `{! Compat_Bindt_Binddt nat T U}
    `{! Compat_Bindd_Binddt nat T U}
    `{! Compat_Mapdt_Binddt nat T U}.

  Context
    `{Module_inst: ! DecoratedTraversableRightPreModule nat T U
                        (unit := Monoid_unit_zero)
                        (op := Monoid_op_plus)}.

  Lemma toLN_loc_None_iff:
    forall k d n, toLN_loc k (d, n) = None <-> n >= d /\ ~ (n - d < length k).T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (k : key) (d n : nat),
toLN_loc k (d, n) = None <->
n >= d /\ ~ n - d < length k
  Proof.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (k : key) (d n : nat),
toLN_loc k (d, n) = None <->
n >= d /\ ~ n - d < length k
    intros.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
toLN_loc k (d, n) = None <->
n >= d /\ ~ n - d < length k
    unfold toLN_loc.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
(if bound_b n d == true
 then Some (Bd n)
 else map Fr (getName k (n - d))) = None <->
n >= d /\ ~ n - d < length k
    unfold bound_b, bound_within_b.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
(if PeanoNat.Nat.ltb n (d + 0) == true
 then Some (Bd n)
 else map Fr (getName k (n - d))) = None <->
n >= d /\ ~ n - d < length k
    replace (d + 0) with d by lia.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
(if PeanoNat.Nat.ltb n d == true
 then Some (Bd n)
 else map Fr (getName k (n - d))) = None <->
n >= d /\ ~ n - d < length k
    remember (Nat.ltb n d) as b.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
b: bool
Heqb: b = Nat.ltb n d
(if b == true
 then Some (Bd n)
 else map Fr (getName k (n - d))) = None <->
n >= d /\ ~ n - d < length k
    symmetry in Heqb.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
b: bool
Heqb: Nat.ltb n d = b
(if b == true
 then Some (Bd n)
 else map Fr (getName k (n - d))) = None <->
n >= d /\ ~ n - d < length k
    destruct b.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: Nat.ltb n d = true
(if true == true
 then Some (Bd n)
 else map Fr (getName k (n - d))) = None <->
n >= d /\ ~ n - d < length k
T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: Nat.ltb n d = false
(if false == true
 then Some (Bd n)
 else map Fr (getName k (n - d))) = None <->
n >= d /\ ~ n - d < length k
    -T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: Nat.ltb n d = true
(if true == true
 then Some (Bd n)
 else map Fr (getName k (n - d))) = None <->
n >= d /\ ~ n - d < length k cbn.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: Nat.ltb n d = true
Some (Bd n) = None <-> n >= d /\ ~ n - d < length k
      rewrite PeanoNat.Nat.ltb_lt in Heqb.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: n < d
Some (Bd n) = None <-> n >= d /\ ~ n - d < length k
      split; intro contra.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: n < d
contra: Some (Bd n) = None
n >= d /\ ~ n - d < length k
T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: n < d
contra: n >= d /\ ~ n - d < length k
Some (Bd n) = None
      +T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: n < d
contra: Some (Bd n) = None
n >= d /\ ~ n - d < length k false.
      +T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: n < d
contra: n >= d /\ ~ n - d < length k
Some (Bd n) = None false.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: n < d
contra: n >= d /\ ~ n - d < length k
False lia.
    -T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: Nat.ltb n d = false
(if false == true
 then Some (Bd n)
 else map Fr (getName k (n - d))) = None <->
n >= d /\ ~ n - d < length k cbn.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: Nat.ltb n d = false
map Fr (getName k (n - d)) = None <->
n >= d /\ ~ n - d < length k
      rewrite PeanoNat.Nat.ltb_ge in Heqb.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: d <= n
map Fr (getName k (n - d)) = None <->
n >= d /\ ~ n - d < length k
      rewrite map_None_eq_iff.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: d <= n
getName k (n - d) = None <->
n >= d /\ ~ n - d < length k
      rewrite <- key_lookup_ix_None_iff.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: d <= n
~ contains_ix_upto (n - d) k <->
n >= d /\ ~ n - d < length k
      unfold contains_ix_upto.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
d, n: nat
Heqb: d <= n
~ n - d < length k <-> n >= d /\ ~ n - d < length k
      split; now auto.
  Qed.

  Lemma toLN_None_iff:
    forall k (t: U nat), toLN k t = None <-> ~ cl_at (length k) t.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (k : key) (t : U nat),
toLN k t = None <-> ~ cl_at (length k) t
  Proof.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (k : key) (t : U nat),
toLN k t = None <-> ~ cl_at (length k) t
    intros.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U nat
toLN k t = None <-> ~ cl_at (length k) t
    rewrite cl_at_spec_not.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U nat
toLN k t = None <->
(exists d n : nat,
   element_ctx_of (d, n) t /\
   ~ cl_at_loc (length k) (d, n))
    unfold toLN.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U nat
mapdt (toLN_loc k) t = None <->
(exists d n : nat,
   element_ctx_of (d, n) t /\
   ~ cl_at_loc (length k) (d, n))
    rewrite mapdt_option_None_spec.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U nat
(exists e a : nat,
   element_ctx_of (e, a) t /\ toLN_loc k (e, a) = None) <->
(exists d n : nat,
   element_ctx_of (d, n) t /\
   ~ cl_at_loc (length k) (d, n))
    setoid_rewrite toLN_loc_None_iff.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U nat
(exists e a : nat,
   element_ctx_of (e, a) t /\
   a >= e /\ ~ a - e < length k) <->
(exists d n : nat,
   element_ctx_of (d, n) t /\
   ~ cl_at_loc (length k) (d, n))
    unfold cl_at_loc, bound_within.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U nat
(exists e a : nat,
   element_ctx_of (e, a) t /\
   a >= e /\ ~ a - e < length k) <->
(exists d n : nat,
   element_ctx_of (d, n) t /\ ~ n < d + length k)
    split; intros [e [a [Hin Hspec]]].T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U nat
e, a: nat
Hin: element_ctx_of (e, a) t
Hspec: a >= e /\ ~ a - e < length k
exists d n : nat,
  element_ctx_of (d, n) t /\ ~ n < d + length k
T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U nat
e, a: nat
Hin: element_ctx_of (e, a) t
Hspec: ~ a < e + length k
exists e a : nat,
  element_ctx_of (e, a) t /\
  a >= e /\ ~ a - e < length k
    -T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U nat
e, a: nat
Hin: element_ctx_of (e, a) t
Hspec: a >= e /\ ~ a - e < length k
exists d n : nat,
  element_ctx_of (d, n) t /\ ~ n < d + length k exists e a; split; auto.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U nat
e, a: nat
Hin: element_ctx_of (e, a) t
Hspec: a >= e /\ ~ a - e < length k
~ a < e + length k lia.
    -T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U nat
e, a: nat
Hin: element_ctx_of (e, a) t
Hspec: ~ a < e + length k
exists e a : nat,
  element_ctx_of (e, a) t /\
  a >= e /\ ~ a - e < length k exists e a; split; auto.T: Type -> Type
Return_T: Return T
Map_T: Map T
Bind_TT: Bind T T
Traverse_T: Traverse T
Mapd_T: Mapd nat T
Bindt_TT: Bindt T T
Bindd_T: Bindd nat T T
Mapdt_T: Mapdt nat T
Binddt_TT: Binddt nat T T
Compat_Map_Binddt0: Compat_Map_Binddt nat T T
Compat_Bind_Binddt0: Compat_Bind_Binddt nat T T
Compat_Traverse_Binddt0: Compat_Traverse_Binddt nat T
  T
Compat_Mapd_Binddt0: Compat_Mapd_Binddt nat T T
Compat_Bindt_Binddt0: Compat_Bindt_Binddt nat T T
Compat_Bindd_Binddt0: Compat_Bindd_Binddt nat T T
Compat_Mapdt_Binddt0: Compat_Mapdt_Binddt nat T T
Monad_inst: DecoratedTraversableMonad nat T
U: Type -> Type
Map_U: Map U
Bind_TU: Bind T U
Traverse_U: Traverse U
Mapd_U: Mapd nat U
Bindt_TU: Bindt T U
Bindd_TU: Bindd nat T U
Mapdt_U: Mapdt nat U
Binddt_TU: Binddt nat T U
Compat_Map_Binddt1: Compat_Map_Binddt nat T U
Compat_Bind_Binddt1: Compat_Bind_Binddt nat T U
Compat_Traverse_Binddt1: Compat_Traverse_Binddt nat T
  U
Compat_Mapd_Binddt1: Compat_Mapd_Binddt nat T U
Compat_Bindt_Binddt1: Compat_Bindt_Binddt nat T U
Compat_Bindd_Binddt1: Compat_Bindd_Binddt nat T U
Compat_Mapdt_Binddt1: Compat_Mapdt_Binddt nat T U
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U nat
e, a: nat
Hin: element_ctx_of (e, a) t
Hspec: ~ a < e + length k
a >= e /\ ~ a - e < length k lia.
  Qed.

End theory.