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
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
  Backends.Adapters.LNtoDB
  Backends.Adapters.DBtoLN
  Functors.Option
  Misc.PartialBijection.

From Coq Require Import PeanoNat.

Import LN.Notations.

Import DecoratedTraversableMonad.UsefulInstances.

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


Section translate.

  Context
    `{Return_T: Return T}
    `{Binddt_TT: Binddt nat T T}
    `{Binddt_TU: Binddt nat T U}
    `{Monad_inst: ! DecoratedTraversableMonad nat T}
    `{Module_inst: ! DecoratedTraversableRightPreModule nat T U
    (unit := Monoid_unit_zero)
    (op := Monoid_op_plus)}.

  (** ** Basic supporting lemmas *)
  (********************************************************************)
  Lemma lc_bound: forall t e n,
      LC (U := U) t ->
      (e, Bd n) ∈d t ->
      bound n e.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U LN) (e n : nat),
LC t -> (e, Bd n) ∈d t -> bound n e
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U LN) (e n : nat),
LC t -> (e, Bd n) ∈d t -> bound n e
    introv HLC Hin.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
e, n: nat
HLC: LC t
Hin: (e, Bd n) ∈d t
bound n e cbn.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
e, n: nat
HLC: LC t
Hin: (e, Bd n) ∈d t
bound n e
    rewrite LC_spec in HLC.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
e, n: nat
HLC: forall (w : nat) (l : LN),
(w, l) ∈d t -> lc_loc 0 (w, l)
Hin: (e, Bd n) ∈d t
bound n e
    specialize (HLC e (Bd n) Hin).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
e, n: nat
HLC: lc_loc 0 (e, Bd n)
Hin: (e, Bd n) ∈d t
bound n e
    unfold lc_loc in HLC.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
e, n: nat
HLC: n < e + 0
Hin: (e, Bd n) ∈d t
bound n e
    replace (e + 0) with e in * by lia.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
e, n: nat
HLC: n < e
Hin: (e, Bd n) ∈d t
bound n e
    destruct e.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
n: nat
HLC: n < 0
Hin: (0, Bd n) ∈d t
bound n 0
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
e, n: nat
HLC: n < S e
Hin: (S e, Bd n) ∈d t
bound n (S e)
    lia.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
e, n: nat
HLC: n < S e
Hin: (S e, Bd n) ∈d t
bound n (S e) unfold bound, bound_within.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
e, n: nat
HLC: n < S e
Hin: (S e, Bd n) ∈d t
n < S e + 0
    lia.
  Qed.

  Lemma lc_bound_b: forall t e n,
      LC (U := U) t ->
      (e, Bd n) ∈d t ->
      bound_b n e = true.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U LN) (e n : nat),
LC t -> (e, Bd n) ∈d t -> bound_b n e = true
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U LN) (e n : nat),
LC t -> (e, Bd n) ∈d t -> bound_b n e = true
    intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
e, n: nat
H: LC t
H0: (e, Bd n) ∈d t
bound_b n e = true specialize (lc_bound t _ _ H H0).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
e, n: nat
H: LC t
H0: (e, Bd n) ∈d t
bound n e -> bound_b n e = true
    rewrite bound_spec.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
e, n: nat
H: LC t
H0: (e, Bd n) ∈d t
bound n e -> n < e
    unfold bound, bound_within.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
e, n: nat
H: LC t
H0: (e, Bd n) ∈d t
n < e + 0 -> n < e
    lia.
  Qed.

  Lemma bound_in_plus: forall n depth,
      ~ bound (n + depth) depth.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall n depth : nat, ~ bound (n + depth) depth
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall n depth : nat, ~ bound (n + depth) depth
    intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
n, depth: nat
~ bound (n + depth) depth unfold bound, bound_within.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
n, depth: nat
~ n + depth < depth + 0 lia.
  Qed.

  Lemma bound_in_plus_b: forall n depth,
      bound_b (n + depth) depth = false.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall n depth : nat,
bound_b (n + depth) depth = false
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall n depth : nat,
bound_b (n + depth) depth = false
    intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
n, depth: nat
bound_b (n + depth) depth = false
    rewrite bound_spec_not.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
n, depth: nat
~ n + depth < depth
    lia.
  Qed.

  Lemma toDB_Fr: forall (n: nat) (a: atom) (k: key),
      a ∈ k ->
      exists ix, toDB_loc k (n, Fr a) = Some ix.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (n : nat) (a : atom) (k : key),
a ∈ k ->
exists ix : nat, toDB_loc k (n, Fr a) = Some ix
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (n : nat) (a : atom) (k : key),
a ∈ k ->
exists ix : nat, toDB_loc k (n, Fr a) = Some ix
    intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
n: nat
a: atom
k: key
H: a ∈ k
exists ix : nat, toDB_loc k (n, Fr a) = Some ix
    unfold toDB_loc.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
n: nat
a: atom
k: key
H: a ∈ k
exists ix : nat,
  map (fun ix0 : nat => ix0 + n) (getIndex k a) =
  Some ix
    lookup atom a in key k.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
n: nat
a: atom
k: key
H, H_in: a ∈ k
n0: nat
H_key_lookup: getIndex k a = Some n0
exists ix : nat,
  map (fun ix0 : nat => ix0 + n) (getIndex k a) =
  Some ix
    rewrite H_key_lookup.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
n: nat
a: atom
k: key
H, H_in: a ∈ k
n0: nat
H_key_lookup: getIndex k a = Some n0
exists ix : nat,
  map (fun ix0 : nat => ix0 + n) (Some n0) = Some ix
    eexists.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
n: nat
a: atom
k: key
H, H_in: a ∈ k
n0: nat
H_key_lookup: getIndex k a = Some n0
map (fun ix : nat => ix + n) (Some n0) = Some ?ix reflexivity.
  Qed.

  (** ** Totality *)
  (********************************************************************)
  (** Given a locally closed locally nameless term and a key with enough atoms,
      <<toDB>> is guaranteed to return something. *)
  Lemma to_DB_from_key_total:
    forall (t: U LN) (k: key),
      LC t ->
      scoped_key k t ->
      exists (t': U nat), toDB k t = Some t'.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U LN) (k : key),
LC t ->
scoped_key k t ->
exists t' : U nat, toDB k t = Some t'
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U LN) (k : key),
LC t ->
scoped_key k t ->
exists t' : U nat, toDB k t = Some t'
    introv HLC Hin.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
HLC: LC t
Hin: scoped_key k t
exists t' : U nat, toDB k t = Some t'
    unfold toDB.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
HLC: LC t
Hin: scoped_key k t
exists t' : U nat, mapdt (toDB_loc k) t = Some t'
    rewrite DecoratedTraversableFunctor.mapdt_through_runBatch.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
HLC: LC t
Hin: scoped_key k t
exists t' : U nat,
  (runBatch (toDB_loc k) ∘ toBatch3) t = Some t'
    unfold compose at 1.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
HLC: LC t
Hin: scoped_key k t
exists t' : U nat,
  runBatch (toDB_loc k) (toBatch3 t) = Some t'
    unfold scoped_key in Hin.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
HLC: LC t
Hin: forall x : atom, x ∈ free t -> x ∈ k
exists t' : U nat,
  runBatch (toDB_loc k) (toBatch3 t) = Some t'
    unfold element_of in Hin.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
HLC: LC t
Hin: forall x : atom,
tosubset (free t) x -> tosubset k x
exists t' : U nat,
  runBatch (toDB_loc k) (toBatch3 t) = Some t'
    unfold LC, LCn in HLC.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
HLC: Forall_ctx (lc_loc 0) t
Hin: forall x : atom,
tosubset (free t) x -> tosubset k x
exists t' : U nat,
  runBatch (toDB_loc k) (toBatch3 t) = Some t'
    rewrite (tosubset_through_runBatch2 _ nat) in Hin.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
HLC: Forall_ctx (lc_loc 0) t
Hin: forall x : atom,
(runBatch ret ∘ toBatch) (free t) x ->
(runBatch ret ∘ toBatch) k x
exists t' : U nat,
  runBatch (toDB_loc k) (toBatch3 t) = Some t'
    (* the proof breaks here because can't rewrite under the binders. *)
    try setoid_rewrite (element_ctx_of_toctxset (E := nat) (T := U)) in HLC.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
HLC: Forall_ctx (lc_loc 0) t
Hin: forall x : atom,
(runBatch ret ∘ toBatch) (free t) x ->
(runBatch ret ∘ toBatch) k x
exists t' : U nat,
  runBatch (toDB_loc k) (toBatch3 t) = Some t'
    (*
    try rewrite (toctxset_through_runBatch2) in HLC.
    rewrite toBatch_to_toBatch3 in Hin.
    unfold compose in Hin.
    induction (toBatch3 t).
    - cbv. eauto.
    - rewrite runBatch_rw2.
      assert (H: (forall x: atom,
                     @runBatch LN nat (@const Type Type (LN -> Prop))
                       (@Map_const (LN -> Prop))
                       (@Mult_const (LN -> Prop) (@Monoid_op_subset LN))
                       (@Pure_const (LN -> Prop) (@Monoid_unit_subset LN))
                       (@ret subset Return_subset LN) (nat -> C)
                       (@mapfst_Batch nat (nat -> C) (nat * LN) LN
                          (@extract (prod nat) (Extract_reader nat) LN) b)
                       (Fr x) -> x ∈ k)).
      { intros x.
        specialize (Hin x).
        intros hyp.
        apply Hin.
        left.
        assumption. }
      specialize (IHb H).
      destruct IHb as [f Hfeq].
      rewrite Hfeq.
      destruct a as [depth l].
      destruct l.
      + pose toDB_Fr.
        specialize (e depth n k).
        enough (H_a_in_k: n ∈ k).
        { specialize (e H_a_in_k).
          destruct e as [ix Hixeq].
          rewrite Hixeq.
          cbn.
          eauto. }
        apply Hin.
        cbn. right.
        reflexivity.
      + (* Proof missing due to technical difficulties above *)
     *)
  Abort.

  Lemma mapdt_None:
    forall (A B: Type) (t: T A) (f: nat * A -> option B),
      (exists (n: nat) (a: A), (n, a) ∈d t /\ f (n, a) = None) ->
      mapdt f t = None.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (A B : Type) (t : T A)
  (f : nat * A -> option B),
(exists (n : nat) (a : A),
   (n, a) ∈d t /\ f (n, a) = None) -> mapdt f t = None
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (A B : Type) (t : T A)
  (f : nat * A -> option B),
(exists (n : nat) (a : A),
   (n, a) ∈d t /\ f (n, a) = None) -> mapdt f t = None
    intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
A, B: Type
t: T A
f: nat * A -> option B
H: exists (n : nat) (a : A),
  (n, a) ∈d t /\ f (n, a) = None
mapdt f t = None
    rewrite mapdt_through_runBatch.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
A, B: Type
t: T A
f: nat * A -> option B
H: exists (n : nat) (a : A),
  (n, a) ∈d t /\ f (n, a) = None
(runBatch (map ret ∘ f) ∘ toBatch7) t = None
  Abort.

  Lemma to_DB_from_key_None:
    forall (t: U LN) (k: key),
      (exists (x: atom), Fr x ∈ t /\ ~ x ∈ k) ->
      toDB k t = None.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U LN) (k : key),
(exists x : atom, Fr x ∈ t /\ ~ x ∈ k) ->
toDB k t = None
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U LN) (k : key),
(exists x : atom, Fr x ∈ t /\ ~ x ∈ k) ->
toDB k t = None
    intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
H: exists x : atom, Fr x ∈ t /\ ~ x ∈ k
toDB k t = None unfold scoped_key in H.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
H: exists x : atom, Fr x ∈ t /\ ~ x ∈ k
toDB k t = None
  Abort.


  (** ** Roundtrip from LN *)
  (********************************************************************)

  (** A helper lemma used below *)
  Lemma LN_DB_roundtrip_loc_helper1: forall k depth x,
      x ∈ k ->
      map (F := option)
        (toLN_loc k ∘ pair depth ∘ (fun ix: nat => ix + depth))
        (getIndex k x) = Some (Some (Fr x)).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (k : list atom) (depth : nat) (x : atom),
x ∈ k ->
map
  (toLN_loc k ∘ pair depth
   ∘ (fun ix : nat => ix + depth)) (getIndex k x) =
Some (Some (Fr x))
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (k : list atom) (depth : nat) (x : atom),
x ∈ k ->
map
  (toLN_loc k ∘ pair depth
   ∘ (fun ix : nat => ix + depth)) (getIndex k x) =
Some (Some (Fr x))
    intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
depth: nat
x: atom
H: x ∈ k
map
  (toLN_loc k ∘ pair depth
   ∘ (fun ix : nat => ix + depth)) (getIndex k x) =
Some (Some (Fr x))
    lookup atom x in key k.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
depth: nat
x: atom
H, H_in: x ∈ k
n: nat
H_key_lookup: getIndex k x = Some n
map
  (toLN_loc k ∘ pair depth
   ∘ (fun ix : nat => ix + depth)) (getIndex k x) =
Some (Some (Fr x))
    rewrite H_key_lookup.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
depth: nat
x: atom
H, H_in: x ∈ k
n: nat
H_key_lookup: getIndex k x = Some n
map
  (toLN_loc k ∘ pair depth
   ∘ (fun ix : nat => ix + depth)) (Some n) =
Some (Some (Fr x))
    change (map ?f (Some ?n)) with (Some (f n)).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
depth: nat
x: atom
H, H_in: x ∈ k
n: nat
H_key_lookup: getIndex k x = Some n
Some
  ((toLN_loc k ∘ pair depth
    ∘ (fun ix : nat => ix + depth)) n) =
Some (Some (Fr x))
    unfold compose, toLN_loc.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
depth: nat
x: atom
H, H_in: x ∈ k
n: nat
H_key_lookup: getIndex k x = Some n
Some
  (if bound_b (n + depth) depth == true
   then Some (Bd (n + depth))
   else map Fr (getName k (n + depth - depth))) =
Some (Some (Fr x))
    rewrite bound_in_plus_b.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
depth: nat
x: atom
H, H_in: x ∈ k
n: nat
H_key_lookup: getIndex k x = Some n
Some
  (if false == true
   then Some (Bd (n + depth))
   else map Fr (getName k (n + depth - depth))) =
Some (Some (Fr x))
    replace (n + depth - depth) with n by lia.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
depth: nat
x: atom
H, H_in: x ∈ k
n: nat
H_key_lookup: getIndex k x = Some n
Some
  (if false == true
   then Some (Bd (n + depth))
   else map Fr (getName k n)) = Some (Some (Fr x))
    rewrite (key_bijection1 x k n H_key_lookup).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
depth: nat
x: atom
H, H_in: x ∈ k
n: nat
H_key_lookup: getIndex k x = Some n
Some
  (if false == true
   then Some (Bd (n + depth))
   else map Fr (Some x)) = Some (Some (Fr x))
    reflexivity.
  Qed.

  (** Starting with a locally closed term and a big enough key,
      the roundtrip is locally the identity function *)
  Lemma LN_DB_roundtrip_loc: forall (t: U LN) k depth l,
      LC t ->
      scoped_key k t ->
      (depth, l) ∈d t ->
      (toLN_loc k ⋆3 toDB_loc k) (depth, l) = pure (F := option ∘ option) l.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U LN) (k : key) (depth : nat) (l : LN),
LC t ->
scoped_key k t ->
(depth, l) ∈d t ->
(toLN_loc k ⋆3 toDB_loc k) (depth, l) = pure l
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U LN) (k : key) (depth : nat) (l : LN),
LC t ->
scoped_key k t ->
(depth, l) ∈d t ->
(toLN_loc k ⋆3 toDB_loc k) (depth, l) = pure l
    introv Hlc Hwhole Hin.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth: nat
l: LN
Hlc: LC t
Hwhole: scoped_key k t
Hin: (depth, l) ∈d t
(toLN_loc k ⋆3 toDB_loc k) (depth, l) = pure l
    rewrite kc3_spec.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth: nat
l: LN
Hlc: LC t
Hwhole: scoped_key k t
Hin: (depth, l) ∈d t
map (toLN_loc k ∘ pair depth) (toDB_loc k (depth, l)) =
pure l
    unfold scoped_key in Hwhole.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth: nat
l: LN
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, l) ∈d t
map (toLN_loc k ∘ pair depth) (toDB_loc k (depth, l)) =
pure l
    destruct l as [x|n].T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth: nat
x: atom
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Fr x) ∈d t
map (toLN_loc k ∘ pair depth)
  (toDB_loc k (depth, Fr x)) = pure (Fr x)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth, n: nat
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Bd n) ∈d t
map (toLN_loc k ∘ pair depth)
  (toDB_loc k (depth, Bd n)) = 
pure (Bd n)
    -T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth: nat
x: atom
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Fr x) ∈d t
map (toLN_loc k ∘ pair depth)
  (toDB_loc k (depth, Fr x)) = pure (Fr x) rewrite toDB_loc_rw2.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth: nat
x: atom
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Fr x) ∈d t
map (toLN_loc k ∘ pair depth)
  (map (fun ix : nat => ix + depth) (getIndex k x)) =
pure (Fr x)
      compose near (getIndex k x).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth: nat
x: atom
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Fr x) ∈d t
(map (toLN_loc k ∘ pair depth)
 ∘ map (fun ix : nat => ix + depth)) (getIndex k x) =
pure (Fr x)
      rewrite (fun_map_map (F := option)).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth: nat
x: atom
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Fr x) ∈d t
map
  (toLN_loc k ∘ pair depth
   ∘ (fun ix : nat => ix + depth)) (getIndex k x) =
pure (Fr x)
      apply ind_implies_in in Hin.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth: nat
x: atom
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: Fr x ∈ t
map
  (toLN_loc k ∘ pair depth
   ∘ (fun ix : nat => ix + depth)) (getIndex k x) =
pure (Fr x)
      rewrite <- in_free_iff in Hin.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth: nat
x: atom
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: x ∈ free t
map
  (toLN_loc k ∘ pair depth
   ∘ (fun ix : nat => ix + depth)) (getIndex k x) =
pure (Fr x)
      specialize (Hwhole x Hin); clear Hin.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth: nat
x: atom
Hlc: LC t
Hwhole: x ∈ k
map
  (toLN_loc k ∘ pair depth
   ∘ (fun ix : nat => ix + depth)) (getIndex k x) =
pure (Fr x)
      now apply LN_DB_roundtrip_loc_helper1.
    -T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth, n: nat
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Bd n) ∈d t
map (toLN_loc k ∘ pair depth)
  (toDB_loc k (depth, Bd n)) = pure (Bd n) rewrite toDB_loc_rw1.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth, n: nat
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Bd n) ∈d t
map (toLN_loc k ∘ pair depth) (Some n) = pure (Bd n)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth, n: nat
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Bd n) ∈d t
n < depth
      change (map ?f (Some ?n)) with (Some (f n)).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth, n: nat
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Bd n) ∈d t
Some ((toLN_loc k ∘ pair depth) n) = pure (Bd n)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth, n: nat
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Bd n) ∈d t
n < depth
      unfold compose.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth, n: nat
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Bd n) ∈d t
Some (toLN_loc k (depth, n)) = pure (Bd n)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth, n: nat
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Bd n) ∈d t
n < depth
      unfold toLN_loc.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth, n: nat
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Bd n) ∈d t
Some
  (if bound_b n depth == true
   then Some (Bd n)
   else map Fr (getName k (n - depth))) = pure (Bd n)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth, n: nat
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Bd n) ∈d t
n < depth
      now rewrite (lc_bound_b t depth n Hlc Hin).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth, n: nat
Hlc: LC t
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Bd n) ∈d t
n < depth
      rewrite LC_spec in Hlc.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth, n: nat
Hlc: forall (w : nat) (l : LN),
(w, l) ∈d t -> lc_loc 0 (w, l)
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Bd n) ∈d t
n < depth
      specialize (Hlc depth (Bd n) Hin).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth, n: nat
Hlc: lc_loc 0 (depth, Bd n)
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Bd n) ∈d t
n < depth
      unfold lc_loc in Hlc.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
depth, n: nat
Hlc: n < depth + 0
Hwhole: forall x : atom, x ∈ free t -> x ∈ k
Hin: (depth, Bd n) ∈d t
n < depth
      lia.
  Qed.

  (** Starting with a locally closed term and a big enough key,
      the roundtrip is locally the identity function *)
  Theorem LN_DB_roundtrip:
    forall (t: U LN) (k: key),
      scoped_key k t ->
      LC t ->
      map (F := option) (toLN k) (toDB k t) =
        Some (Some t).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U LN) (k : key),
scoped_key k t ->
LC t -> map (toLN k) (toDB k t) = Some (Some t)
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U LN) (k : key),
scoped_key k t ->
LC t -> map (toLN k) (toDB k t) = Some (Some t)
    intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
H: scoped_key k t
H0: LC t
map (toLN k) (toDB k t) = Some (Some t)
    unfold toLN.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
H: scoped_key k t
H0: LC t
map (mapdt (toLN_loc k)) (toDB k t) = Some (Some t)
    unfold toDB.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
H: scoped_key k t
H0: LC t
map (mapdt (toLN_loc k)) (mapdt (toDB_loc k) t) =
Some (Some t)
    compose near t on left.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
H: scoped_key k t
H0: LC t
(map (mapdt (toLN_loc k)) ∘ mapdt (toDB_loc k)) t =
Some (Some t)
    rewrite mapdt_mapdt.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
H: scoped_key k t
H0: LC t
mapdt (toLN_loc k ⋆3 toDB_loc k) t = Some (Some t)
    change (Some (Some t)) with (pure (F := option ∘ option) t).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
H: scoped_key k t
H0: LC t
mapdt (toLN_loc k ⋆3 toDB_loc k) t = pure t
    apply (mapdt_respectful_pure _ (G := option ∘ option)).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
H: scoped_key k t
H0: LC t
forall (e : nat) (a : LN),
(e, a) ∈d t ->
(toLN_loc k ⋆3 toDB_loc k) (e, a) = pure a
    intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U LN
k: key
H: scoped_key k t
H0: LC t
e: nat
a: LN
H1: (e, a) ∈d t
(toLN_loc k ⋆3 toDB_loc k) (e, a) = pure a
    rewrite (LN_DB_roundtrip_loc t); auto.
  Qed.

  (** ** Roundtrip from DB *)
  (********************************************************************)

  (** A helper lemma used below *)
  Lemma DB_LN_roundtrip_loc_helper1:
    forall (t:U nat) k gap (GapNotZero: gap <> 0) depth (n:nat),
      unique k ->
       n < depth + gap ->
       resolves_gap gap k ->
      bound_b n depth = false ->
      (depth, n) ∈d t ->
      map (toDB_loc k ∘ pair depth) (map Fr (getName k (n - depth))) = Some (Some n).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U nat) (k : list atom) (gap : nat),
gap <> 0 ->
forall depth n : nat,
unique k ->
n < depth + gap ->
resolves_gap gap k ->
bound_b n depth = false ->
(depth, n) ∈d t ->
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n)
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U nat) (k : list atom) (gap : nat),
gap <> 0 ->
forall depth n : nat,
unique k ->
n < depth + gap ->
resolves_gap gap k ->
bound_b n depth = false ->
(depth, n) ∈d t ->
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n)
    introv Hnz Huniq Hclosed Hcont Hbound Helt.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Hcont: resolves_gap gap k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n)
    unfold toLN_loc.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Hcont: resolves_gap gap k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n)
    rewrite resolves_gap_spec in Hcont.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Hcont: contains_ix_upto (gap - 1) k \/ gap = 0
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n)
    assert (n >= depth).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Hcont: contains_ix_upto (gap - 1) k \/ gap = 0
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
n >= depth
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Hcont: contains_ix_upto (gap - 1) k \/ gap = 0
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = 
Some (Some n)
    {T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Hcont: contains_ix_upto (gap - 1) k \/ gap = 0
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
n >= depth unfold bound, bound_within in Hbound.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Hcont: contains_ix_upto (gap - 1) k \/ gap = 0
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
n >= depth
      apply PeanoNat.Nat.ltb_ge in Hbound.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Hcont: contains_ix_upto (gap - 1) k \/ gap = 0
Hbound: depth + 0 <= n
Helt: (depth, n) ∈d t
n >= depth
      lia.
    }T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Hcont: contains_ix_upto (gap - 1) k \/ gap = 0
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n)
    destruct Hcont as [Okay | GapZero].T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
GapZero: gap = 0
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = 
Some (Some n)
    {T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n) remember (getName k (n - depth)).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
o: option atom
Heqo: o = getName k (n - depth)
map (toDB_loc k ∘ pair depth) (map Fr o) =
Some (Some n)
      symmetry in Heqo.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
o: option atom
Heqo: getName k (n - depth) = o
map (toDB_loc k ∘ pair depth) (map Fr o) =
Some (Some n)
      destruct o.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
n0: atom
Heqo: getName k (n - depth) = Some n0
map (toDB_loc k ∘ pair depth) (map Fr (Some n0)) =
Some (Some n)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
Heqo: getName k (n - depth) = None
map (toDB_loc k ∘ pair depth) (map Fr None) =
Some (Some n)
      {T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
n0: atom
Heqo: getName k (n - depth) = Some n0
map (toDB_loc k ∘ pair depth) (map Fr (Some n0)) =
Some (Some n) cbn.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
n0: atom
Heqo: getName k (n - depth) = Some n0
Some
  (map (fun ix : nat => ix + depth) (getIndex k n0)) =
Some (Some n)
        rewrite key_bijection in Heqo; auto.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
n0: atom
Heqo: getIndex k n0 = Some (n - depth)
Some
  (map (fun ix : nat => ix + depth) (getIndex k n0)) =
Some (Some n)
        rewrite Heqo.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
n0: atom
Heqo: getIndex k n0 = Some (n - depth)
Some
  (map (fun ix : nat => ix + depth) (Some (n - depth))) =
Some (Some n)
        cbn.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
n0: atom
Heqo: getIndex k n0 = Some (n - depth)
Some (Some (n - depth + depth)) = Some (Some n)
        fequal.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
n0: atom
Heqo: getIndex k n0 = Some (n - depth)
Some (n - depth + depth) = Some n fequal.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
n0: atom
Heqo: getIndex k n0 = Some (n - depth)
n - depth + depth = n lia.
      }T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
Heqo: getName k (n - depth) = None
map (toDB_loc k ∘ pair depth) (map Fr None) =
Some (Some n)
      {T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
Heqo: getName k (n - depth) = None
map (toDB_loc k ∘ pair depth) (map Fr None) =
Some (Some n) cbn.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
Heqo: getName k (n - depth) = None
None = Some (Some n) false.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
Heqo: getName k (n - depth) = None
False
        apply key_lookup_ix_None1 in Heqo.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: contains_ix_upto (gap - 1) k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
Heqo: ~ contains_ix_upto (n - depth) k
False
        unfold contains_ix_upto in *.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Okay: gap - 1 < length k
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
Heqo: ~ n - depth < length k
False lia.
      }
    }T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
GapZero: gap = 0
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n)
    {T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap: nat
Hnz: gap <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
GapZero: gap = 0
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n) subst.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
Hnz: 0 <> 0
depth, n: nat
Huniq: unique k
Hclosed: n < depth + 0
Hbound: bound_b n depth = false
Helt: (depth, n) ∈d t
H: n >= depth
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n) false. }
  Qed.

  (** A helper lemma used below *)
  Lemma DB_LN_roundtrip_loc: forall (t:U nat) k gap depth (n:nat),
      unique k ->
      cl_at gap t ->
      resolves_gap gap k ->
      (depth, n) ∈d t ->
      (toDB_loc k ⋆3 toLN_loc k) (depth, n) =
        pure (F := option ∘ option) n.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U nat) (k : list atom) (gap depth n : nat),
unique k ->
cl_at gap t ->
resolves_gap gap k ->
(depth, n) ∈d t ->
(toDB_loc k ⋆3 toLN_loc k) (depth, n) = pure n
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (t : U nat) (k : list atom) (gap depth n : nat),
unique k ->
cl_at gap t ->
resolves_gap gap k ->
(depth, n) ∈d t ->
(toDB_loc k ⋆3 toLN_loc k) (depth, n) = pure n
    introv Huniq Hclosed Hcont Helt.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
(toDB_loc k ⋆3 toLN_loc k) (depth, n) = pure n
    unfold_ops @Pure_compose @Pure_option.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
(toDB_loc k ⋆3 toLN_loc k) (depth, n) = Some (Some n)
    rewrite kc3_spec.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
map (toDB_loc k ∘ pair depth) (toLN_loc k (depth, n)) =
Some (Some n)
    unfold toLN_loc.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
map (toDB_loc k ∘ pair depth)
  (if bound_b n depth == true
   then Some (Bd n)
   else map Fr (getName k (n - depth))) =
Some (Some n)
    bound_induction.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
Hord: n >= depth
Hbound: bound_b n depth = false
map (toDB_loc k ∘ pair depth)
  (if false == true
   then Some (Bd n)
   else map Fr (getName k (n - depth))) =
Some (Some n)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
Hord: n < depth
Hbound: bound_b n depth = true
map (toDB_loc k ∘ pair depth)
  (if true == true
   then Some (Bd n)
   else map Fr (getName k (n - depth))) =
Some (Some n)
    {T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
Hord: n >= depth
Hbound: bound_b n depth = false
map (toDB_loc k ∘ pair depth)
  (if false == true
   then Some (Bd n)
   else map Fr (getName k (n - depth))) =
Some (Some n) cbn.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
Hord: n >= depth
Hbound: bound_b n depth = false
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n)
      rewrite cl_at_spec in Hclosed.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: forall d n : nat,
(d, n) ∈d t -> cl_at_loc gap (d, n)
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
Hord: n >= depth
Hbound: bound_b n depth = false
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n)
      specialize (Hclosed depth n Helt).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at_loc gap (depth, n)
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
Hord: n >= depth
Hbound: bound_b n depth = false
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n)
      unfold cl_at_loc, bound_within in Hclosed.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
Hord: n >= depth
Hbound: bound_b n depth = false
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n)
      assert (gap <> 0) by lia. (* nothing is less than zero. *)T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: n < depth + gap
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
Hord: n >= depth
Hbound: bound_b n depth = false
H: gap <> 0
map (toDB_loc k ∘ pair depth)
  (map Fr (getName k (n - depth))) = Some (Some n)
      apply (DB_LN_roundtrip_loc_helper1 t k gap); eauto.
    }T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
Hord: n < depth
Hbound: bound_b n depth = true
map (toDB_loc k ∘ pair depth)
  (if true == true
   then Some (Bd n)
   else map Fr (getName k (n - depth))) =
Some (Some n)
    {T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
Hord: n < depth
Hbound: bound_b n depth = true
map (toDB_loc k ∘ pair depth)
  (if true == true
   then Some (Bd n)
   else map Fr (getName k (n - depth))) =
Some (Some n) cbn.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (depth, n) ∈d t
Hord: n < depth
Hbound: bound_b n depth = true
Some
  (if
    match depth with
    | 0 => false
    | S m' => n <=? m'
    end
   then Some n
   else None) = Some (Some n)
      destruct depth.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (0, n) ∈d t
Hord: n < 0
Hbound: bound_b n 0 = true
Some None = Some (Some n)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (S depth, n) ∈d t
Hord: n < S depth
Hbound: bound_b n (S depth) = true
Some (if n <=? depth then Some n else None) =
Some (Some n)
      -T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (0, n) ∈d t
Hord: n < 0
Hbound: bound_b n 0 = true
Some None = Some (Some n) false.
      -T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (S depth, n) ∈d t
Hord: n < S depth
Hbound: bound_b n (S depth) = true
Some (if n <=? depth then Some n else None) =
Some (Some n) assert (Hle: n <= depth) by lia.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (S depth, n) ∈d t
Hord: n < S depth
Hbound: bound_b n (S depth) = true
Hle: n <= depth
Some (if n <=? depth then Some n else None) =
Some (Some n)
        rewrite <- Nat.leb_le in Hle.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (S depth, n) ∈d t
Hord: n < S depth
Hbound: bound_b n (S depth) = true
Hle: (n <=? depth) = true
Some (if n <=? depth then Some n else None) =
Some (Some n)
        rewrite Hle.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
t: U nat
k: list atom
gap, depth, n: nat
Huniq: unique k
Hclosed: cl_at gap t
Hcont: resolves_gap gap k
Helt: (S depth, n) ∈d t
Hord: n < S depth
Hbound: bound_b n (S depth) = true
Hle: (n <=? depth) = true
Some (Some n) = Some (Some n)
        reflexivity.
    }
  Qed.

  (** Starting with a term with no more than <<gap>>-level free variables, if the key has at least <<gap>> many unique
      names, the roundtrip of a de Bruijn index is locally the identity function. *)
  Theorem DB_LN_roundtrip: forall k gap (t: U nat),
      unique k ->
      cl_at gap t ->
      resolves_gap gap k ->
      map (F := option) (toDB k) (toLN k t) =
        Some (Some t).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (k : list atom) (gap : nat) (t : U nat),
unique k ->
cl_at gap t ->
resolves_gap gap k ->
map (toDB k) (toLN k t) = Some (Some t)
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (k : list atom) (gap : nat) (t : U nat),
unique k ->
cl_at gap t ->
resolves_gap gap k ->
map (toDB k) (toLN k t) = Some (Some t)
    intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
gap: nat
t: U nat
H: unique k
H0: cl_at gap t
H1: resolves_gap gap k
map (toDB k) (toLN k t) = Some (Some t)
    unfold toLN.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
gap: nat
t: U nat
H: unique k
H0: cl_at gap t
H1: resolves_gap gap k
map (toDB k) (mapdt (toLN_loc k) t) = Some (Some t)
    unfold toDB.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
gap: nat
t: U nat
H: unique k
H0: cl_at gap t
H1: resolves_gap gap k
map (mapdt (toDB_loc k)) (mapdt (toLN_loc k) t) =
Some (Some t)
    compose near t on left.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
gap: nat
t: U nat
H: unique k
H0: cl_at gap t
H1: resolves_gap gap k
(map (mapdt (toDB_loc k)) ∘ mapdt (toLN_loc k)) t =
Some (Some t)
    rewrite mapdt_mapdt.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
gap: nat
t: U nat
H: unique k
H0: cl_at gap t
H1: resolves_gap gap k
mapdt (toDB_loc k ⋆3 toLN_loc k) t = Some (Some t)
    all: try typeclasses eauto.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
gap: nat
t: U nat
H: unique k
H0: cl_at gap t
H1: resolves_gap gap k
mapdt (toDB_loc k ⋆3 toLN_loc k) t = Some (Some t)
    change (Some (Some t)) with (pure (F := option ∘ option) t).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
gap: nat
t: U nat
H: unique k
H0: cl_at gap t
H1: resolves_gap gap k
mapdt (toDB_loc k ⋆3 toLN_loc k) t = pure t
    apply (mapdt_respectful_pure _ (G := option ∘ option)).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
gap: nat
t: U nat
H: unique k
H0: cl_at gap t
H1: resolves_gap gap k
forall e a : nat,
(e, a) ∈d t ->
(toDB_loc k ⋆3 toLN_loc k) (e, a) = pure a
    intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
gap: nat
t: U nat
H: unique k
H0: cl_at gap t
H1: resolves_gap gap k
e, a: nat
H2: (e, a) ∈d t
(toDB_loc k ⋆3 toLN_loc k) (e, a) = pure a
    now rewrite (DB_LN_roundtrip_loc t k gap).
  Qed.

  Theorem DB_LN_partial_bijection_iff: forall k,
      unique k ->
      (forall (t: U LN) (u: U nat),
          toDB k t = Some u <-> toLN k u = Some t).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall k : list atom,
unique k ->
forall (t : U LN) (u : U nat),
toDB k t = Some u <-> toLN k u = Some t
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall k : list atom,
unique k ->
forall (t : U LN) (u : U nat),
toDB k t = Some u <-> toLN k u = Some t
    intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
u: U nat
toDB k t = Some u <-> toLN k u = Some t
    apply partial_bijection_spec.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
u: U nat
(forall b : U nat,
 toLN k b = None \/
 map (toDB k) (toLN k b) = Some (Some b)) /\
(forall a : U LN,
 toDB k a = None \/
 map (toLN k) (toDB k a) = Some (Some a))
    clear t u.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
(forall b : U nat,
 toLN k b = None \/
 map (toDB k) (toLN k b) = Some (Some b)) /\
(forall a : U LN,
 toDB k a = None \/
 map (toLN k) (toDB k a) = Some (Some a)) split; intros t.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
toLN k t = None \/
map (toDB k) (toLN k t) = Some (Some t)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
toDB k t = None \/
map (toLN k) (toDB k t) = Some (Some t)
    -T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
toLN k t = None \/
map (toDB k) (toLN k t) = Some (Some t) rewrite toLN_None_iff.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
~ cl_at (length k) t \/
map (toDB k) (toLN k t) = Some (Some t)
      destruct (cl_at_decidable (length k) t) as [Hclosedat | Not_Hclosedat].T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
Hclosedat: cl_at (length k) t
~ cl_at (length k) t \/
map (toDB k) (toLN k t) = Some (Some t)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
Not_Hclosedat: ~ cl_at (length k) t
~ cl_at (length k) t \/
map (toDB k) (toLN k t) = Some (Some t)
      right.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
Hclosedat: cl_at (length k) t
map (toDB k) (toLN k t) = Some (Some t)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
Not_Hclosedat: ~ cl_at (length k) t
~ cl_at (length k) t \/
map (toDB k) (toLN k t) = Some (Some t)
      eapply (DB_LN_roundtrip k (length k)).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
Hclosedat: cl_at (length k) t
unique k
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
Hclosedat: cl_at (length k) t
cl_at (length k) t
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
Hclosedat: cl_at (length k) t
resolves_gap (length k) k
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
Not_Hclosedat: ~ cl_at (length k) t
~ cl_at (length k) t \/
map (toDB k) (toLN k t) = Some (Some t)
      +T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
Hclosedat: cl_at (length k) t
unique k assumption.
      +T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
Hclosedat: cl_at (length k) t
cl_at (length k) t assumption.
      +T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
Hclosedat: cl_at (length k) t
resolves_gap (length k) k unfold resolves_gap.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
Hclosedat: cl_at (length k) t
length k <= length k lia.
      +T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U nat
Not_Hclosedat: ~ cl_at (length k) t
~ cl_at (length k) t \/
map (toDB k) (toLN k t) = Some (Some t) now left.
    -T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
toDB k t = None \/
map (toLN k) (toDB k t) = Some (Some t) rewrite toDB_None_iff2.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
(~ scoped_key k t \/ ~ LC t) \/
map (toLN k) (toDB k t) = Some (Some t)
      destruct (scoped_key_decidable k t).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
H0: scoped_key k t
(~ scoped_key k t \/ ~ LC t) \/
map (toLN k) (toDB k t) = Some (Some t)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
H0: ~ scoped_key k t
(~ scoped_key k t \/ ~ LC t) \/
map (toLN k) (toDB k t) = Some (Some t)
      {T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
H0: scoped_key k t
(~ scoped_key k t \/ ~ LC t) \/
map (toLN k) (toDB k t) = Some (Some t) destruct (LC_decidable t).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
H0: scoped_key k t
H1: LC t
(~ scoped_key k t \/ ~ LC t) \/
map (toLN k) (toDB k t) = Some (Some t)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
H0: scoped_key k t
H1: ~ LC t
(~ scoped_key k t \/ ~ LC t) \/
map (toLN k) (toDB k t) = Some (Some t)
        {T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
H0: scoped_key k t
H1: LC t
(~ scoped_key k t \/ ~ LC t) \/
map (toLN k) (toDB k t) = Some (Some t) right.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
H0: scoped_key k t
H1: LC t
map (toLN k) (toDB k t) = Some (Some t) apply LN_DB_roundtrip; assumption. }T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
H0: scoped_key k t
H1: ~ LC t
(~ scoped_key k t \/ ~ LC t) \/
map (toLN k) (toDB k t) = Some (Some t)
        {T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
H0: scoped_key k t
H1: ~ LC t
(~ scoped_key k t \/ ~ LC t) \/
map (toLN k) (toDB k t) = Some (Some t) left.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
H0: scoped_key k t
H1: ~ LC t
~ scoped_key k t \/ ~ LC t now right. }
      }T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
H0: ~ scoped_key k t
(~ scoped_key k t \/ ~ LC t) \/
map (toLN k) (toDB k t) = Some (Some t)
      {T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
H0: ~ scoped_key k t
(~ scoped_key k t \/ ~ LC t) \/
map (toLN k) (toDB k t) = Some (Some t) left.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: list atom
H: unique k
t: U LN
H0: ~ scoped_key k t
~ scoped_key k t \/ ~ LC t now left. }
  Qed.

  Lemma not_scoped_LC_iff: forall (k: key) (t: U LN),
      ~ (scoped_key k t /\ LC t) <-> ~ scoped_key k t \/ ~ LC t.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (k : key) (t : U LN),
~ (scoped_key k t /\ LC t) <->
~ scoped_key k t \/ ~ LC t
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall (k : key) (t : U LN),
~ (scoped_key k t /\ LC t) <->
~ scoped_key k t \/ ~ LC t
    intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U LN
~ (scoped_key k t /\ LC t) <->
~ scoped_key k t \/ ~ LC t
    split.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U LN
~ (scoped_key k t /\ LC t) ->
~ scoped_key k t \/ ~ LC t
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U LN
~ scoped_key k t \/ ~ LC t ->
~ (scoped_key k t /\ LC t)
    -T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U LN
~ (scoped_key k t /\ LC t) ->
~ scoped_key k t \/ ~ LC t intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U LN
H: ~ (scoped_key k t /\ LC t)
~ scoped_key k t \/ ~ LC t
      apply Decidable.not_and.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U LN
H: ~ (scoped_key k t /\ LC t)
Decidable.decidable (scoped_key k t)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U LN
H: ~ (scoped_key k t /\ LC t)
~ (scoped_key k t /\ LC t)
      apply scoped_key_decidable.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U LN
H: ~ (scoped_key k t /\ LC t)
~ (scoped_key k t /\ LC t)
      assumption.
    -T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
t: U LN
~ scoped_key k t \/ ~ LC t ->
~ (scoped_key k t /\ LC t) tauto.
  Qed.

  Theorem DB_LN_partial_bijection:
    forall (k: key),
      unique k ->
      PartialBijectionSpec
        (U LN) (U nat)
        (fun t => (forall (x: atom), x ∈ free t -> x ∈ k) /\ LC t)
        (fun t => level t <= length k)
        (toDB k) (toLN k).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall k : key,
unique k ->
PartialBijectionSpec (U LN) (U nat)
  (fun t : U LN =>
   (forall x : atom, x ∈ free t -> x ∈ k) /\ LC t)
  (fun t : U nat => level t <= length k) (toDB k)
  (toLN k)
  Proof.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
forall k : key,
unique k ->
PartialBijectionSpec (U LN) (U nat)
  (fun t : U LN =>
   (forall x : atom, x ∈ free t -> x ∈ k) /\ LC t)
  (fun t : U nat => level t <= length k) (toDB k)
  (toLN k)
    intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
PartialBijectionSpec (U LN) (U nat)
  (fun t : U LN =>
   (forall x : atom, x ∈ free t -> x ∈ k) /\ LC t)
  (fun t : U nat => level t <= length k) (toDB k)
  (toLN k)
    constructor.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
forall (a : U LN) (b : U nat),
toDB k a = Some b <-> toLN k b = Some a
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
forall a : U LN,
toDB k a = None <->
~ ((forall x : atom, x ∈ free a -> x ∈ k) /\ LC a)
T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
forall b : U nat,
toLN k b = None <-> ~ level b <= length k
    -T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
forall (a : U LN) (b : U nat),
toDB k a = Some b <-> toLN k b = Some a intros.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
a: U LN
b: U nat
toDB k a = Some b <-> toLN k b = Some a
      apply DB_LN_partial_bijection_iff.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
a: U LN
b: U nat
unique k
      assumption.
    -T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
forall a : U LN,
toDB k a = None <->
~ ((forall x : atom, x ∈ free a -> x ∈ k) /\ LC a) intros t.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
t: U LN
toDB k t = None <->
~ ((forall x : atom, x ∈ free t -> x ∈ k) /\ LC t)
      rewrite toDB_None_iff2.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
t: U LN
~ scoped_key k t \/ ~ LC t <->
~ ((forall x : atom, x ∈ free t -> x ∈ k) /\ LC t)
      rewrite <- (not_scoped_LC_iff k t).T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
t: U LN
~ (scoped_key k t /\ LC t) <->
~ ((forall x : atom, x ∈ free t -> x ∈ k) /\ LC t)
      unfold scoped_key.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
t: U LN
~ ((forall x : atom, x ∈ free t -> x ∈ k) /\ LC t) <->
~ ((forall x : atom, x ∈ free t -> x ∈ k) /\ LC t)
      reflexivity.
    -T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
forall b : U nat,
toLN k b = None <-> ~ level b <= length k intros t.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
t: U nat
toLN k t = None <-> ~ level t <= length k
      rewrite toLN_None_iff.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
t: U nat
~ cl_at (length k) t <-> ~ level t <= length k
      rewrite level_iff.T: Type -> Type
Return_T: Return T
Binddt_TT: Binddt nat T T
U: Type -> Type
Binddt_TU: Binddt nat T U
Monad_inst: DecoratedTraversableMonad nat T
Module_inst: DecoratedTraversableRightPreModule nat T
  U
k: key
H: unique k
t: U nat
~ level t <= length k <-> ~ level t <= length k
      reflexivity.
  Qed.

End translate.