SystemF_LN.v

From Tealeaves Require Export
  Examples.SystemF.Syntax
  Simplification.Tests.Support
  Simplification.MBinddt
  Simplification.Tests.SystemF_Binddt
  Simplification.Tests.SystemF_Targeted
  Classes.Multisorted.Theory.Foldmap.

#[local] Generalizable Variables G.
#[local] Arguments mbinddt {ix} {W}%type_scope {T} U%function_scope
  {MBind} {F}%function_scope {H H0 H1 A B} _ _.

#[local] Generalizable Variables A B C F W T U K.

Section local_lemmas_needed.

  Context
    (U : Type -> Type)
      `{MultiDecoratedTraversablePreModule (list K) T U
          (mn_op := Monoid_op_list)
          (mn_unit := Monoid_unit_list)}
      `{! MultiDecoratedTraversableMonad (list K) T
          (mn_op := Monoid_op_list)
          (mn_unit := Monoid_unit_list)}.

  Lemma subst_to_kbind : forall (k: K) (x: atom) (u: T k LN),
      subst U k x u = kbind U k (subst_loc k x u).U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (x : atom) (u : T k LN),
subst U k x u = kbind U k (subst_loc k x u)
  Proof.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (x : atom) (u : T k LN),
subst U k x u = kbind U k (subst_loc k x u)
    reflexivity.
  Qed.

  Lemma open_to_kbindd : forall (k: K) (u: T k LN),
      open U k u = kbindd U k (open_loc k u).U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (u : T k LN),
open U k u = kbindd U k (open_loc k u)
  Proof.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (u : T k LN),
open U k u = kbindd U k (open_loc k u)
    reflexivity.
  Qed.

  Lemma free_to_mapReducek : forall (k: K),
      free U (T := T) k = mapReducek U k free_loc.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall k : K, free U k = mapReducek U k free_loc
  Proof.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall k : K, free U k = mapReducek U k free_loc
    intros.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
free U k = mapReducek U k free_loc
    unfold free.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
bind free_loc ○ toklist U k = mapReducek U k free_loc ext t.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
bind free_loc (toklist U k t) =
mapReducek U k free_loc t
    unfold toklist, compose.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
bind free_loc (map extract (toklistd U k t)) =
mapReducek U k free_loc t
    unfold mapReducek.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
bind free_loc (map extract (toklistd U k t)) =
mapReducem U (tgt_def k free_loc (const Ƶ)) t
    rewrite mapReducem_to_mapReducemd.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
bind free_loc (map extract (toklistd U k t)) =
mapReducemd U
  (tgt_def k free_loc (const Ƶ) ◻ allK extract) t
    rewrite (mapReducemd_through_tolist U).U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
bind free_loc (map extract (toklistd U k t)) =
(mapReduce_list
   (fun '(w, (k0, a)) =>
    (tgt_def k free_loc (const Ƶ) ◻ allK extract) k0
      (w, a)) ∘ tolistmd U) t
    unfold toklistd.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
bind free_loc
  (map extract ((filterk k ∘ tolistmd U) t)) =
(mapReduce_list
   (fun '(w, (k0, a)) =>
    (tgt_def k free_loc (const Ƶ) ◻ allK extract) k0
      (w, a)) ∘ tolistmd U) t
    unfold compose.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
bind free_loc (map extract (filterk k (tolistmd U t))) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   (tgt_def k free_loc (const Ƶ) ◻ allK extract) k0
     (w, a)) (tolistmd U t)
    induction (tolistmd U t).U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
bind free_loc (map extract (filterk k [])) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   (tgt_def k free_loc (const Ƶ) ◻ allK extract) k0
     (w, a)) []
U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
a: list K * (K * LN)
l: list (list K * (K * LN))
IHl: bind free_loc (map extract (filterk k l)) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   (tgt_def k free_loc (const Ƶ) ◻ allK extract)
     k0 (w, a)) l
bind free_loc (map extract (filterk k (a :: l))) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   (tgt_def k free_loc (const Ƶ) ◻ allK extract) k0
     (w, a)) 
  (a :: l)
    -U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
bind free_loc (map extract (filterk k [])) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   (tgt_def k free_loc (const Ƶ) ◻ allK extract) k0
     (w, a)) [] reflexivity.
    -U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
a: list K * (K * LN)
l: list (list K * (K * LN))
IHl: bind free_loc (map extract (filterk k l)) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   (tgt_def k free_loc (const Ƶ) ◻ allK extract)
     k0 (w, a)) l
bind free_loc (map extract (filterk k (a :: l))) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   (tgt_def k free_loc (const Ƶ) ◻ allK extract) k0
     (w, a)) (a :: l) destruct a as [w [j l']].U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
w: list K
j: K
l': LN
l: list (list K * (K * LN))
IHl: bind free_loc (map extract (filterk k l)) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   (tgt_def k free_loc (const Ƶ) ◻ allK extract)
     k0 (w, a)) l
bind free_loc
  (map extract (filterk k ((w, (j, l')) :: l))) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   (tgt_def k free_loc (const Ƶ) ◻ allK extract) k0
     (w, a)) ((w, (j, l')) :: l)
      cbn.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
w: list K
j: K
l': LN
l: list (list K * (K * LN))
IHl: bind free_loc (map extract (filterk k l)) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   (tgt_def k free_loc (const Ƶ) ◻ allK extract)
     k0 (w, a)) l
bind free_loc
  (map extract
     (if k == j
      then (w, l') :: filterk k l
      else filterk k l)) =
(tgt_def k free_loc (const Ƶ) ◻ allK extract) j
  (w, l')
● crush_list
    (map
       (fun '(w, (k0, a)) =>
        (tgt_def k free_loc (const Ƶ) ◻ allK extract)
          k0 (w, a)) l)
      unfold tgt_def.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
w: list K
j: K
l': LN
l: list (list K * (K * LN))
IHl: bind free_loc (map extract (filterk k l)) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   (tgt_def k free_loc (const Ƶ) ◻ allK extract)
     k0 (w, a)) l
bind free_loc
  (map extract
     (if k == j
      then (w, l') :: filterk k l
      else filterk k l)) =
((fun j : K => if k == j then free_loc else const Ƶ)
 ◻ allK extract) j (w, l')
● crush_list
    (map
       (fun '(w, (k0, a)) =>
        ((fun j : K =>
          if k == j then free_loc else const Ƶ)
         ◻ allK extract) k0 (w, a)) l)
      unfold_ops @Monoid_op_list.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
w: list K
j: K
l': LN
l: list (list K * (K * LN))
IHl: bind free_loc (map extract (filterk k l)) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   (tgt_def k free_loc (const Ƶ) ◻ allK extract)
     k0 (w, a)) l
bind free_loc
  (map extract
     (if k == j
      then (w, l') :: filterk k l
      else filterk k l)) =
((fun j : K => if k == j then free_loc else const Ƶ)
 ◻ allK extract) j (w, l') ++
crush_list
  (map
     (fun '(w, (k0, a)) =>
      ((fun j : K =>
        if k == j then free_loc else const Ƶ)
       ◻ allK extract) k0 (w, a)) l)
      unfold vec_compose, compose.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
w: list K
j: K
l': LN
l: list (list K * (K * LN))
IHl: bind free_loc (map extract (filterk k l)) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   (tgt_def k free_loc (const Ƶ) ◻ allK extract)
     k0 (w, a)) l
bind free_loc
  (map extract
     (if k == j
      then (w, l') :: filterk k l
      else filterk k l)) =
(if k == j then free_loc else const Ƶ)
  (allK extract j (w, l')) ++
crush_list
  (map
     (fun '(w, (k0, a)) =>
      (if k == k0 then free_loc else const Ƶ)
        (allK extract k0 (w, a))) l)
      cbn.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: U LN
w: list K
j: K
l': LN
l: list (list K * (K * LN))
IHl: bind free_loc (map extract (filterk k l)) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   (tgt_def k free_loc (const Ƶ) ◻ allK extract)
     k0 (w, a)) l
bind free_loc
  (map extract
     (if k == j
      then (w, l') :: filterk k l
      else filterk k l)) =
(if k == j then free_loc else const Ƶ) l' ++
crush_list
  (map
     (fun '(_, (k0, a)) =>
      (if k == k0 then free_loc else const Ƶ) a) l) destruct_eq_args k j.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
t: U LN
w: list K
j: K
l': LN
l: list (list K * (K * LN))
IHl: bind free_loc (map extract (filterk j l)) =
mapReduce_list
  (fun '(w, (k, a)) =>
   (tgt_def j free_loc (const Ƶ) ◻ allK extract)
     k (w, a)) l
DESTR_EQs: j = j
bind free_loc (map extract ((w, l') :: filterk j l)) =
free_loc l' ++
crush_list
  (map
     (fun '(_, (k, a)) =>
      (if j == k then free_loc else const Ƶ) a) l)
      cbn.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
t: U LN
w: list K
j: K
l': LN
l: list (list K * (K * LN))
IHl: bind free_loc (map extract (filterk j l)) =
mapReduce_list
  (fun '(w, (k, a)) =>
   (tgt_def j free_loc (const Ƶ) ◻ allK extract)
     k (w, a)) l
DESTR_EQs: j = j
free_loc l'
● bind free_loc (map extract (filterk j l)) =
free_loc l' ++
crush_list
  (map
     (fun '(_, (k, a)) =>
      (if j == k then free_loc else const Ƶ) a) l) rewrite IHl.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
t: U LN
w: list K
j: K
l': LN
l: list (list K * (K * LN))
IHl: bind free_loc (map extract (filterk j l)) =
mapReduce_list
  (fun '(w, (k, a)) =>
   (tgt_def j free_loc (const Ƶ) ◻ allK extract)
     k (w, a)) l
DESTR_EQs: j = j
free_loc l'
● mapReduce_list
    (fun '(w, (k, a)) =>
     (tgt_def j free_loc (const Ƶ) ◻ allK extract) k
       (w, a)) l =
free_loc l' ++
crush_list
  (map
     (fun '(_, (k, a)) =>
      (if j == k then free_loc else const Ƶ) a) l) fequal.
  Qed.

  Lemma FV_to_free : forall (k: K) (t: U LN),
      FV U k t = atoms (free U (T := T) k t).U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : U LN),
FV U k t = atoms (free U k t)
  Proof.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : U LN),
FV U k t = atoms (free U k t)
    reflexivity.
  Qed.

  Lemma LCn_to_Forallkd:
    forall (n: nat) (t: U LN) k,
      LCn U k n t = Forallkd U k (lc_loc k n) t.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (n : nat) (t : U LN) (k : K),
LCn U k n t = Forallkd U k (lc_loc k n) t
  Proof.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (n : nat) (t : U LN) (k : K),
LCn U k n t = Forallkd U k (lc_loc k n) t
    intros.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
n: nat
t: U LN
k: K
LCn U k n t = Forallkd U k (lc_loc k n) t
    apply propositional_extensionality.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
n: nat
t: U LN
k: K
LCn U k n t <-> Forallkd U k (lc_loc k n) t
    rewrite <- (Forallkd_spec U (lc_loc k n)).U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
n: nat
t: U LN
k: K
LCn U k n t <->
(forall (w : list K) (a : LN),
 (w, (k, a)) ∈md t -> lc_loc k n (w, a))
    reflexivity.
  Qed.

  Lemma LC_to_Forallkd:
    forall (n: nat) (t: U LN) k,
      LC U k t = Forallkd U k (lc_loc k 0) t.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
nat ->
forall (t : U LN) (k : K),
LC U k t = Forallkd U k (lc_loc k 0) t
  Proof.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
nat ->
forall (t : U LN) (k : K),
LC U k t = Forallkd U k (lc_loc k 0) t
    intros.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
n: nat
t: U LN
k: K
LC U k t = Forallkd U k (lc_loc k 0) t
    apply propositional_extensionality.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
n: nat
t: U LN
k: K
LC U k t <-> Forallkd U k (lc_loc k 0) t
    rewrite <- (Forallkd_spec U (lc_loc k 0)).U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
n: nat
t: U LN
k: K
LC U k t <->
(forall (w : list K) (a : LN),
 (w, (k, a)) ∈md t -> lc_loc k 0 (w, a))
    reflexivity.
  Qed.

  Lemma lc_loc_preincr_eq :
    forall k n j,
      k = j ->
      (lc_loc k n ⦿ [j]) =
        lc_loc k (S n).U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (n : nat) (j : K),
k = j -> lc_loc k n ⦿ [j] = lc_loc k (S n)
  Proof.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (n : nat) (j : K),
k = j -> lc_loc k n ⦿ [j] = lc_loc k (S n)
    intros.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k = j
lc_loc k n ⦿ [j] = lc_loc k (S n)
    unfold preincr, compose, incr.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k = j
(fun a : list K * LN =>
 lc_loc k n (let '(w1, a0) := a in ([j] ● w1, a0))) =
lc_loc k (S n)
    ext [w l].U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k = j
w: list K
l: LN
lc_loc k n ([j] ● w, l) = lc_loc k (S n) (w, l)
    unfold lc_loc.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k = j
w: list K
l: LN
match l with
| Fr _ => True
| Bd n0 => n0 < countk k ([j] ● w) + n
end =
match l with
| Fr _ => True
| Bd n0 => n0 < countk k w + S n
end
    destruct l as [x | m].U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k = j
w: list K
x: atom
True = True
U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k = j
w: list K
m: nat
(m < countk k ([j] ● w) + n) = (m < countk k w + S n)
    -U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k = j
w: list K
x: atom
True = True reflexivity.
    -U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k = j
w: list K
m: nat
(m < countk k ([j] ● w) + n) = (m < countk k w + S n) cbn.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k = j
w: list K
m: nat
(m < (if k == j then 1 else 0) + countk k w + n) =
(m < countk k w + S n) destruct_eq_args k j.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
n: nat
j: K
w: list K
m: nat
DESTR_EQs, DESTR_EQ: j = j
(m < 1 + countk j w + n) = (m < countk j w + S n)
      propext; lia.
  Qed.

  Lemma lc_loc_preincr_neq :
    forall k n j,
      k <> j ->
      (lc_loc k n ⦿ [j]) =
        lc_loc k n.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (n : nat) (j : K),
k <> j -> lc_loc k n ⦿ [j] = lc_loc k n
  Proof.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (n : nat) (j : K),
k <> j -> lc_loc k n ⦿ [j] = lc_loc k n
    intros.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k <> j
lc_loc k n ⦿ [j] = lc_loc k n
    unfold preincr, compose, incr.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k <> j
(fun a : list K * LN =>
 lc_loc k n (let '(w1, a0) := a in ([j] ● w1, a0))) =
lc_loc k n
    ext [w l].U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k <> j
w: list K
l: LN
lc_loc k n ([j] ● w, l) = lc_loc k n (w, l)
    unfold lc_loc.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k <> j
w: list K
l: LN
match l with
| Fr _ => True
| Bd n0 => n0 < countk k ([j] ● w) + n
end =
match l with
| Fr _ => True
| Bd n0 => n0 < countk k w + n
end
    destruct l as [x | m].U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k <> j
w: list K
x: atom
True = True
U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k <> j
w: list K
m: nat
(m < countk k ([j] ● w) + n) = (m < countk k w + n)
    -U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k <> j
w: list K
x: atom
True = True reflexivity.
    -U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k <> j
w: list K
m: nat
(m < countk k ([j] ● w) + n) = (m < countk k w + n) cbn.U: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T U
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
n: nat
j: K
H1: k <> j
w: list K
m: nat
(m < (if k == j then 1 else 0) + countk k w + n) =
(m < countk k w + n) destruct_eq_args k j.
  Qed.

End local_lemmas_needed.

Create HintDb lc_loc_db.
#[global] Hint Rewrite lc_loc_preincr_eq: lc_loc_db.
#[global] Hint Rewrite lc_loc_preincr_neq: lc_loc_db.

(*
Ltac handle_lc_loc :=
  autorewrite* with lc_loc_db using (auto; try discriminate).
 *)

Ltac handle_lc_loc :=
  match goal with
  | |- context[lc_loc (ix := ?ix)] =>
      first [ rewrite (lc_loc_preincr_eq (ix := ix)) by auto
            | rewrite (lc_loc_preincr_neq (ix := ix)) by
              (solve [auto || discriminate])
        ]
  end.

Ltac simplify_open_pre_refold_hook :=
  idtac.

Ltac simplify_open_post_refold_hook :=
  idtac.

Ltac simplify_open :=
  rewrite ?open_to_kbindd;
  simplify_kbindd;
  simplify_open_pre_refold_hook;
  rewrite <- ?open_to_kbindd;
  simplify_open_post_refold_hook.

(** ** <<open>> *)
(******************************************************************************)
Section rw_open.

  Context
    (A : Type)
      (k : K2)
      (x: atom)
      (u: SystemF k LN).

  Ltac tactic_being_tested ::= simplify_open.

  Lemma open_type_rw1 : forall c,
      open typ k u (ty_c c) = ty_c c.A: Type
k: K2
x: atom
u: SystemF k LN
forall c : base_typ, open typ k u (ty_c c) = ty_c c
  Proof.A: Type
k: K2
x: atom
u: SystemF k LN
forall c : base_typ, open typ k u (ty_c c) = ty_c c
    test_simplification.
  Qed.

  (*
  Lemma open_type_rw2_neq : forall (a : A),
      k <> ktyp ->
      open typ k f (ty_v a) = ty_v a.
  Proof.
    intros.
    simplify_open.
    rewrite btgd_neq; auto.
  Qed.*)

  Lemma open_type_rw3 : forall (t1 t2 : typ LN),
      open typ k u (ty_ar t1 t2) =
        ty_ar (open typ k u t1) (open typ k u t2).A: Type
k: K2
x: atom
u: SystemF k LN
forall t1 t2 : typ LN,
open typ k u (ty_ar t1 t2) =
ty_ar (open typ k u t1) (open typ k u t2)
  Proof.A: Type
k: K2
x: atom
u: SystemF k LN
forall t1 t2 : typ LN,
open typ k u (ty_ar t1 t2) =
ty_ar (open typ k u t1) (open typ k u t2)
    test_simplification.
  Qed.

  Lemma open_type_rw4 : forall (body : typ LN),
      open typ k u (ty_univ body) =
        ty_univ (kbindd typ k (preincr (W := list K) (open_loc k u) [ktyp]) body).A: Type
k: K2
x: atom
u: SystemF k LN
forall body : typ LN,
open typ k u (ty_univ body) =
ty_univ (kbindd typ k (open_loc k u ⦿ [ktyp]) body)
  Proof.A: Type
k: K2
x: atom
u: SystemF k LN
forall body : typ LN,
open typ k u (ty_univ body) =
ty_univ (kbindd typ k (open_loc k u ⦿ [ktyp]) body)
    intros.A: Type
k: K2
x: atom
u: SystemF k LN
body: typ LN
open typ k u (ty_univ body) =
ty_univ (kbindd typ k (open_loc k u ⦿ [ktyp]) body)
    test_simplification.
  Qed.

  Lemma open_term_rw1_neq : forall (a : LN),
      k <> ktrm ->
      open term k u (tm_var a) = tm_var a.A: Type
k: K2
x: atom
u: SystemF k LN
forall a : LN,
k <> ktrm -> open term k u (tm_var a) = tm_var a
  Proof.A: Type
k: K2
x: atom
u: SystemF k LN
forall a : LN,
k <> ktrm -> open term k u (tm_var a) = tm_var a
    intros.A: Type
k: K2
x: atom
u: SystemF k LN
a: LN
H: k <> ktrm
open term k u (tm_var a) = tm_var a
    unfold open.A: Type
k: K2
x: atom
u: SystemF k LN
a: LN
H: k <> ktrm
kbindd term k (open_loc k u) (tm_var a) = tm_var a
    simplify_kbindd.A: Type
k: K2
x: atom
u: SystemF k LN
a: LN
H: k <> ktrm
btgd k (open_loc k u) ktrm ([], a) = tm_var a
    normalize_K.A: Type
k: K2
x: atom
u: SystemF k LN
a: LN
H: k <> ktrm
btgd k (open_loc k u) ktrm ([], a) = tm_var a
  Abort.

  Lemma open_term_rw2 : forall (τ : typ LN) (t : term LN),
      open term k u (tm_abs τ t) =
        tm_abs (open typ k u τ)
          (kbindd term k (preincr (W := list K) (open_loc k u) [ktrm]) t).A: Type
k: K2
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
open term k u (tm_abs τ t) =
tm_abs (open typ k u τ)
  (kbindd term k (open_loc k u ⦿ [ktrm]) t)
  Proof.A: Type
k: K2
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
open term k u (tm_abs τ t) =
tm_abs (open typ k u τ)
  (kbindd term k (open_loc k u ⦿ [ktrm]) t)
    test_simplification.
  Qed.

  Lemma open_term_rw3 : forall (t1 t2 : term LN),
      open term k u (tm_app t1 t2) =
        tm_app (open term k u t1) (open term k u t2).A: Type
k: K2
x: atom
u: SystemF k LN
forall t1 t2 : term LN,
open term k u (tm_app t1 t2) =
tm_app (open term k u t1) (open term k u t2)
  Proof.A: Type
k: K2
x: atom
u: SystemF k LN
forall t1 t2 : term LN,
open term k u (tm_app t1 t2) =
tm_app (open term k u t1) (open term k u t2)
    test_simplification.
  Qed.

  Lemma open_term_rw4 : forall (t : term LN),
      open term k u (tm_tab t) =
        tm_tab (kbindd term k (preincr (W := list K) (open_loc k u) [ktyp]) t).A: Type
k: K2
x: atom
u: SystemF k LN
forall t : term LN,
open term k u (tm_tab t) =
tm_tab (kbindd term k (open_loc k u ⦿ [ktyp]) t)
  Proof.A: Type
k: K2
x: atom
u: SystemF k LN
forall t : term LN,
open term k u (tm_tab t) =
tm_tab (kbindd term k (open_loc k u ⦿ [ktyp]) t)
    test_simplification.
  Qed.

  Lemma open_term_rw5 : forall (t: term LN) (τ : typ LN),
      open term k u (tm_tap t τ) =
        tm_tap (open term k u t) (open typ k u τ).A: Type
k: K2
x: atom
u: SystemF k LN
forall (t : term LN) (τ : typ LN),
open term k u (tm_tap t τ) =
tm_tap (open term k u t) (open typ k u τ)
  Proof.A: Type
k: K2
x: atom
u: SystemF k LN
forall (t : term LN) (τ : typ LN),
open term k u (tm_tap t τ) =
tm_tap (open term k u t) (open typ k u τ)
    test_simplification.
  Qed.

End rw_open.

Ltac simplify_LCn_pre_refold_hook :=
  repeat handle_lc_loc.

Ltac simplify_LCn_post_refold_hook :=
  idtac.

Ltac simplify_LCn :=
  match goal with
  | |- context[LCn (T := ?T) (ix := ?ix)
                ?U ?k ?n ?t] =>
      rewrite ?(LCn_to_Forallkd _(*U*) (ix := ix));
      simplify_Forallkd;
      simplify_LCn_pre_refold_hook;
      rewrite <- ?(LCn_to_Forallkd _ (ix := ix));
      simplify_LCn_post_refold_hook
  end.

(** ** <<LCn>> *)
(******************************************************************************)
Section rw_LCn.

  Context
    (A : Type)
      (k : K2)
      (n: nat)
      (x: atom)
      (u: SystemF k LN).

  Ltac tactic_being_tested ::= simplify_LCn.

  Lemma LCn_type_rw1 : forall c,
      LCn typ k n (ty_c c) = True.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall c : base_typ, LCn typ k n (ty_c c) = True
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall c : base_typ, LCn typ k n (ty_c c) = True
    test_simplification.
  Qed.

  (*
  Lemma LCn_type_rw2_neq : forall (a : A),
      k <> ktyp ->
      LC typ k f (ty_v a) = ty_v a.
  Proof.
    intros.
    simplify_LC.
    rewrite btgd_neq; auto.
  Qed.*)

  Lemma LCn_type_rw3 : forall (t1 t2 : typ LN),
      LCn typ k n (ty_ar t1 t2) =
        (LCn typ k n t1 /\ LCn typ k n t2).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : typ LN,
LCn typ k n (ty_ar t1 t2) =
(LCn typ k n t1 /\ LCn typ k n t2)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : typ LN,
LCn typ k n (ty_ar t1 t2) =
(LCn typ k n t1 /\ LCn typ k n t2)
    test_simplification.
  Qed.

  Lemma LCn_type_rw4_eq : forall (body : typ LN),
      k = ktyp ->
      LCn typ k n (ty_univ body) =
        LCn typ k (S n) body.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall body : typ LN,
k = ktyp ->
LCn typ k n (ty_univ body) = LCn typ k (S n) body
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall body : typ LN,
k = ktyp ->
LCn typ k n (ty_univ body) = LCn typ k (S n) body
    test_simplification.
  Qed.

  Lemma LCn_type_rw4_neq : forall (body : typ LN),
      k <> ktyp ->
      LCn typ k n (ty_univ body) =
        LCn typ k n body.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall body : typ LN,
k <> ktyp ->
LCn typ k n (ty_univ body) = LCn typ k n body
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall body : typ LN,
k <> ktyp ->
LCn typ k n (ty_univ body) = LCn typ k n body
    test_simplification.
  Qed.

  (*
  Lemma LCn_term_rw1_neq : forall (a : LN),
      k <> ktrm ->
      LC term (tm_var a) = tm_var a.
  Proof.
    intros.
    unfold LC.
    simplify_kbindd.
    normalize_K.
  Abort.
  *)

  Lemma LCn_term_rw2_eq : forall (τ : typ LN) (t : term LN),
      k = ktrm ->
      LCn term k n (tm_abs τ t) =
        (LCn typ k n τ /\ LCn term k (S n) t).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
k = ktrm ->
LCn term k n (tm_abs τ t) =
(LCn typ k n τ /\ LCn term k (S n) t)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
k = ktrm ->
LCn term k n (tm_abs τ t) =
(LCn typ k n τ /\ LCn term k (S n) t)
    test_simplification.
  Qed.

  Lemma LCn_term_rw2_neq : forall (τ : typ LN) (t : term LN),
      k <> ktrm ->
      LCn term k n (tm_abs τ t) =
        (LCn typ k n τ /\ LCn term k n t).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
k <> ktrm ->
LCn term k n (tm_abs τ t) =
(LCn typ k n τ /\ LCn term k n t)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
k <> ktrm ->
LCn term k n (tm_abs τ t) =
(LCn typ k n τ /\ LCn term k n t)
    test_simplification.
  Qed.

  Lemma LCn_term_rw3 : forall (t1 t2 : term LN),
      LCn term k n (tm_app t1 t2) =
        (LCn term k n t1 /\ LCn term k n t2).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : term LN,
LCn term k n (tm_app t1 t2) =
(LCn term k n t1 /\ LCn term k n t2)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : term LN,
LCn term k n (tm_app t1 t2) =
(LCn term k n t1 /\ LCn term k n t2)
    test_simplification.
  Qed.

  Lemma LCn_term_rw4_neq : forall (t : term LN),
      k <> ktyp ->
      LCn term k n (tm_tab t) =
        LCn term k n t.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t : term LN,
k <> ktyp -> LCn term k n (tm_tab t) = LCn term k n t
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t : term LN,
k <> ktyp -> LCn term k n (tm_tab t) = LCn term k n t
    test_simplification.
  Qed.

  Lemma LCn_term_rw4_eq : forall (t : term LN),
      k = ktyp ->
      LCn term k n (tm_tab t) =
        LCn term k (S n) t.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t : term LN,
k = ktyp ->
LCn term k n (tm_tab t) = LCn term k (S n) t
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t : term LN,
k = ktyp ->
LCn term k n (tm_tab t) = LCn term k (S n) t
    test_simplification.
  Qed.

  Lemma LCn_term_rw5 : forall (t: term LN) (τ : typ LN),
      LCn term k n (tm_tap t τ) =
        (LCn term k n t /\ LCn typ k n τ).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (t : term LN) (τ : typ LN),
LCn term k n (tm_tap t τ) =
(LCn term k n t /\ LCn typ k n τ)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (t : term LN) (τ : typ LN),
LCn term k n (tm_tap t τ) =
(LCn term k n t /\ LCn typ k n τ)
    test_simplification.
  Qed.

End rw_LCn.

Ltac simplify_LC_pre_refold_hook :=
  idtac.

Ltac simplify_LC_post_refold_hook :=
  idtac.

Ltac simplify_LC :=
  match goal with
  | |- context[LC (T := ?T) (ix := ?ix)
                ?U ?k ?t] =>
      unfold LC;
      simplify_LCn;
      repeat (change (LCn ?U ?k 0) with (LC U k))
  end.

(** ** <<LC>> *)
(******************************************************************************)
Section rw_LC.

  Context
    (A : Type)
      (k : K2)
      (n: nat)
      (x: atom)
      (u: SystemF k LN).

  Ltac tactic_being_tested ::= simplify_LC.

  Lemma LC_type_rw1 : forall c,
      LC typ k (ty_c c) = True.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall c : base_typ, LC typ k (ty_c c) = True
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall c : base_typ, LC typ k (ty_c c) = True
    test_simplification.
  Qed.

  Lemma LC_type_rw3 : forall (t1 t2 : typ LN),
      LC typ k (ty_ar t1 t2) =
        (LC typ k t1 /\ LC typ k t2).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : typ LN,
LC typ k (ty_ar t1 t2) = (LC typ k t1 /\ LC typ k t2)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : typ LN,
LC typ k (ty_ar t1 t2) = (LC typ k t1 /\ LC typ k t2)
    test_simplification.
  Qed.

  Lemma LC_type_rw4_eq : forall (body : typ LN),
      k = ktyp ->
      LC typ k (ty_univ body) =
        LCn typ k 1 body.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall body : typ LN,
k = ktyp -> LC typ k (ty_univ body) = LCn typ k 1 body
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall body : typ LN,
k = ktyp -> LC typ k (ty_univ body) = LCn typ k 1 body
    test_simplification.
  Qed.

  Lemma LC_type_rw4_neq : forall (body : typ LN),
      k <> ktyp ->
      LC typ k (ty_univ body) =
        LC typ k body.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall body : typ LN,
k <> ktyp -> LC typ k (ty_univ body) = LC typ k body
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall body : typ LN,
k <> ktyp -> LC typ k (ty_univ body) = LC typ k body
    test_simplification.
  Qed.

  Lemma LC_term_rw2_eq : forall (τ : typ LN) (t : term LN),
      k = ktrm ->
      LC term k (tm_abs τ t) =
        (LC typ k τ /\ LCn term k 1 t).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
k = ktrm ->
LC term k (tm_abs τ t) =
(LC typ k τ /\ LCn term k 1 t)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
k = ktrm ->
LC term k (tm_abs τ t) =
(LC typ k τ /\ LCn term k 1 t)
    test_simplification.
  Qed.

  Lemma LC_term_rw2_neq : forall (τ : typ LN) (t : term LN),
      k <> ktrm ->
      LC term k (tm_abs τ t) =
        (LC typ k τ /\ LC term k t).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
k <> ktrm ->
LC term k (tm_abs τ t) = (LC typ k τ /\ LC term k t)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
k <> ktrm ->
LC term k (tm_abs τ t) = (LC typ k τ /\ LC term k t)
    test_simplification.
  Qed.

  Lemma LC_term_rw3 : forall (t1 t2 : term LN),
      LC term k (tm_app t1 t2) =
        (LC term k t1 /\ LC term k t2).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : term LN,
LC term k (tm_app t1 t2) =
(LC term k t1 /\ LC term k t2)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : term LN,
LC term k (tm_app t1 t2) =
(LC term k t1 /\ LC term k t2)
    test_simplification.
  Qed.

  Lemma LC_term_rw4_neq : forall (t : term LN),
      k <> ktyp ->
      LC term k (tm_tab t) =
        LC term k t.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t : term LN,
k <> ktyp -> LC term k (tm_tab t) = LC term k t
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t : term LN,
k <> ktyp -> LC term k (tm_tab t) = LC term k t
    test_simplification.
  Qed.

  Lemma LC_term_rw4_eq : forall (t : term LN),
      k = ktyp ->
      LC term k (tm_tab t) =
        LCn term k 1 t.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t : term LN,
k = ktyp -> LC term k (tm_tab t) = LCn term k 1 t
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t : term LN,
k = ktyp -> LC term k (tm_tab t) = LCn term k 1 t
    test_simplification.
  Qed.

  Lemma LC_term_rw5 : forall (t: term LN) (τ : typ LN),
      LC term k (tm_tap t τ) =
        (LC term k t /\ LC typ k τ).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (t : term LN) (τ : typ LN),
LC term k (tm_tap t τ) = (LC term k t /\ LC typ k τ)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (t : term LN) (τ : typ LN),
LC term k (tm_tap t τ) = (LC term k t /\ LC typ k τ)
    test_simplification.
  Qed.

End rw_LC.

Ltac simplify_subst_pre_refold_hook :=
  idtac.

Ltac simplify_subst_post_refold_hook :=
  idtac.

Ltac simplify_subst :=
  match goal with
  | |- context[subst (T := ?T) (ix := ?ix)
                ?U ?k ?t] =>
      rewrite ?(subst_to_kbind);
      simplify_kbind;
      rewrite <- ?(subst_to_kbind)
  end.

(** ** <<subst>> *)
(******************************************************************************)
Section rw_subst.

  Context
    (A : Type)
      (k : K2)
      (n: nat)
      (x: atom)
      (u: SystemF k LN).

  Ltac tactic_being_tested ::= simplify_subst.

  Lemma subst_type_rw1 : forall c,
      subst typ k x u (ty_c c) = ty_c c.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall c : base_typ, subst typ k x u (ty_c c) = ty_c c
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall c : base_typ, subst typ k x u (ty_c c) = ty_c c
    test_simplification.
  Qed.

  Lemma subst_type_rw3 : forall (t1 t2 : typ LN),
      subst typ k x u (ty_ar t1 t2) =
        ty_ar (subst typ k x u t1) (subst typ k x u t2).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : typ LN,
subst typ k x u (ty_ar t1 t2) =
ty_ar (subst typ k x u t1) (subst typ k x u t2)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : typ LN,
subst typ k x u (ty_ar t1 t2) =
ty_ar (subst typ k x u t1) (subst typ k x u t2)
    test_simplification.
  Qed.

  Lemma subst_type_rw4 : forall (body : typ LN),
      subst typ k x u (ty_univ body) =
        ty_univ (subst typ k x u body).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall body : typ LN,
subst typ k x u (ty_univ body) =
ty_univ (subst typ k x u body)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall body : typ LN,
subst typ k x u (ty_univ body) =
ty_univ (subst typ k x u body)
    test_simplification.
  Qed.

  Lemma subst_term_rw2_eq : forall (τ : typ LN) (t : term LN),
      subst term k x u (tm_abs τ t) =
        tm_abs (subst typ k x u τ) (subst term k x u t).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
subst term k x u (tm_abs τ t) =
tm_abs (subst typ k x u τ) (subst term k x u t)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
subst term k x u (tm_abs τ t) =
tm_abs (subst typ k x u τ) (subst term k x u t)
    test_simplification.
  Qed.

  Lemma subst_term_rw2 : forall (τ : typ LN) (t : term LN),
      subst term k x u (tm_abs τ t) =
        tm_abs (subst typ k x u τ) (subst term k x u t).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
subst term k x u (tm_abs τ t) =
tm_abs (subst typ k x u τ) (subst term k x u t)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
subst term k x u (tm_abs τ t) =
tm_abs (subst typ k x u τ) (subst term k x u t)
    test_simplification.
  Qed.

  Lemma subst_term_rw3 : forall (t1 t2 : term LN),
      subst term k x u (tm_app t1 t2) =
        tm_app (subst term k x u t1) (subst term k x u t2).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : term LN,
subst term k x u (tm_app t1 t2) =
tm_app (subst term k x u t1) (subst term k x u t2)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : term LN,
subst term k x u (tm_app t1 t2) =
tm_app (subst term k x u t1) (subst term k x u t2)
    test_simplification.
  Qed.

  Lemma subst_term_rw4 : forall (t : term LN),
      subst term k x u (tm_tab t) =
        tm_tab (subst term k x u t).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t : term LN,
subst term k x u (tm_tab t) =
tm_tab (subst term k x u t)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t : term LN,
subst term k x u (tm_tab t) =
tm_tab (subst term k x u t)
    test_simplification.
  Qed.

  Lemma subst_term_rw5 : forall (t: term LN) (τ : typ LN),
      subst term k x u (tm_tap t τ) =
        tm_tap (subst term k x u t) (subst typ k x u τ).A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (t : term LN) (τ : typ LN),
subst term k x u (tm_tap t τ) =
tm_tap (subst term k x u t) (subst typ k x u τ)
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (t : term LN) (τ : typ LN),
subst term k x u (tm_tap t τ) =
tm_tap (subst term k x u t) (subst typ k x u τ)
    test_simplification.
  Qed.

End rw_subst.

Ltac simplify_free_pre_refold_hook :=
  idtac.

Ltac simplify_free_post_refold_hook :=
  unfold_ops @Monoid_op_list;
  unfold_ops @Monoid_unit_list.

Ltac handle_free_at_leaf :=
  (match goal with
   | |- context[EqDec_eq_of_EqDec ?Keq ?k1 ?k2] =>
       destruct (EqDec_eq_of_EqDec Keq k1 k2);
       try easy
   end).

Ltac simplify_free :=
  match goal with
  | |- context[free (T := ?T) (ix := ?ix)
                ?U ?k ?t] =>
      rewrite ?(free_to_mapReducek _ (ix := ix));
      simplify_mapReducek;
      simplify_free_pre_refold_hook;
      rewrite <- ?(free_to_mapReducek _ (ix := ix));
      simplify_free_post_refold_hook;
      try solve [handle_free_at_leaf]
  end.

(** ** <<free>> *)
(******************************************************************************)
Section rw_free.

  Context
    (A : Type)
      (k : K2)
      (n: nat)
      (x: atom)
      (u: SystemF k LN).

  Ltac tactic_being_tested ::= simplify_free.

  Lemma free_type_rw1 : forall c,
      free typ k (ty_c c) = nil.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall c : base_typ, free typ k (ty_c c) = []
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall c : base_typ, free typ k (ty_c c) = []
    test_simplification.
  Qed.

  Lemma free_type_rw2_atom_eq : forall (x: atom),
      k = ktyp ->
      free typ k (ty_v (Fr x)) = [ x ].A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall x : atom,
k = ktyp -> free typ k (ty_v (Fr x)) = [x]
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall x : atom,
k = ktyp -> free typ k (ty_v (Fr x)) = [x]
    test_simplification.
  Qed.

  Lemma free_type_rw2_atom : forall (x: atom),
      k <> ktyp ->
      free typ k (ty_v (Fr x)) = [ ].A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall x : atom,
k <> ktyp -> free typ k (ty_v (Fr x)) = []
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall x : atom,
k <> ktyp -> free typ k (ty_v (Fr x)) = []
    test_simplification.
  Qed.

  Lemma free_type_rw2_bound : forall n,
      free typ k (ty_v (Bd n)) = [ ].A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall n : nat, free typ k (ty_v (Bd n)) = []
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall n : nat, free typ k (ty_v (Bd n)) = []
    test_simplification.
  Qed.

  Lemma free_type_rw3 : forall (t1 t2 : typ LN),
      free typ k (ty_ar t1 t2) =
        free typ k t1 ++ free typ k t2.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : typ LN,
free typ k (ty_ar t1 t2) =
free typ k t1 ++ free typ k t2
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : typ LN,
free typ k (ty_ar t1 t2) =
free typ k t1 ++ free typ k t2
    test_simplification.
  Qed.

  Lemma free_type_rw4 : forall (body : typ LN),
      free typ k (ty_univ body) =
        free typ k body.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall body : typ LN,
free typ k (ty_univ body) = free typ k body
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall body : typ LN,
free typ k (ty_univ body) = free typ k body
    test_simplification.
  Qed.

  Lemma free_term_rw2_eq : forall (τ : typ LN) (t : term LN),
      free term k (tm_abs τ t) =
        free typ k τ ++ free term k t.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
free term k (tm_abs τ t) =
free typ k τ ++ free term k t
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
free term k (tm_abs τ t) =
free typ k τ ++ free term k t
    test_simplification.
  Qed.

  Lemma free_term_rw2 : forall (τ : typ LN) (t : term LN),
      free term k (tm_abs τ t) =
        free typ k τ ++ free term k t.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
free term k (tm_abs τ t) =
free typ k τ ++ free term k t
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
free term k (tm_abs τ t) =
free typ k τ ++ free term k t
    test_simplification.
  Qed.

  Lemma free_term_rw3 : forall (t1 t2 : term LN),
      free term k (tm_app t1 t2) =
        free term k t1 ++ free term k t2.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : term LN,
free term k (tm_app t1 t2) =
free term k t1 ++ free term k t2
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : term LN,
free term k (tm_app t1 t2) =
free term k t1 ++ free term k t2
    test_simplification.
  Qed.

  Lemma free_term_rw4 : forall (t : term LN),
      free term k (tm_tab t) =
        free term k t.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t : term LN,
free term k (tm_tab t) = free term k t
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t : term LN,
free term k (tm_tab t) = free term k t
    test_simplification.
  Qed.

  Lemma free_term_rw5 : forall (t: term LN) (τ : typ LN),
      free term k (tm_tap t τ) =
        free term k t ++ free typ k τ.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (t : term LN) (τ : typ LN),
free term k (tm_tap t τ) =
free term k t ++ free typ k τ
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (t : term LN) (τ : typ LN),
free term k (tm_tap t τ) =
free term k t ++ free typ k τ
    test_simplification.
  Qed.

End rw_free.

Ltac assert_identical_with_atoms :=
    match goal with
    | |- ?x [=] ?x =>
        ltac_trace "Both sides identical:";
        print_goal
    end.

Ltac test_simplification_with_atoms :=
  intros;
  tactic_being_tested;
  try normalize_K;
  now assert_identical_with_atoms.

Ltac simplify_FV_pre_refold_hook :=
  autorewrite with tea_rw_atoms.

Ltac simplify_FV_post_refold_hook :=
  idtac.

Ltac simplify_FV :=
  match goal with
  | |- context[FV (T := ?T) (ix := ?ix)
                ?U ?k ?t] =>
      rewrite ?(FV_to_free _ (ix := ix));
      simplify_free;
      simplify_FV_pre_refold_hook;
      rewrite <- ?(FV_to_free _ (ix := ix));
      simplify_FV_post_refold_hook
  end.

(** ** <<FV>> *)
(******************************************************************************)
Section rw_FV.

  Context
    (A : Type)
      (k : K2)
      (n: nat)
      (x: atom)
      (u: SystemF k LN).

  Ltac tactic_being_tested ::= simplify_FV.

  #[local] Open Scope set_scope.

  Lemma FV_type_rw1 : forall c,
      FV typ k (ty_c c) [=] ∅.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall c : base_typ, FV typ k (ty_c c) [=] ∅
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall c : base_typ, FV typ k (ty_c c) [=] ∅
    test_simplification_with_atoms.
  Qed.

  Lemma FV_type_rw2_atom : forall (x: atom),
      k = ktyp ->
      FV typ k (ty_v (Fr x)) [=] {{ x }}.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall x : atom,
k = ktyp -> FV typ k (ty_v (Fr x)) [=] {{x}}
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall x : atom,
k = ktyp -> FV typ k (ty_v (Fr x)) [=] {{x}}
    test_simplification_with_atoms.
  Qed.

  Lemma FV_type_rw3 : forall (t1 t2 : typ LN),
      FV typ k (ty_ar t1 t2) [=]
        FV typ k t1 ∪ FV typ k t2.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : typ LN,
FV typ k (ty_ar t1 t2) [=] FV typ k t1 ∪ FV typ k t2
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : typ LN,
FV typ k (ty_ar t1 t2) [=] FV typ k t1 ∪ FV typ k t2
    test_simplification_with_atoms.
  Qed.

  Lemma FV_type_rw4 : forall (body : typ LN),
      FV typ k (ty_univ body) [=]
        FV typ k body.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall body : typ LN,
FV typ k (ty_univ body) [=] FV typ k body
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall body : typ LN,
FV typ k (ty_univ body) [=] FV typ k body
    test_simplification_with_atoms.
  Qed.

  Lemma FV_term_rw2_eq : forall (τ : typ LN) (t : term LN),
      FV term k (tm_abs τ t) [=]
        FV typ k τ ∪ FV term k t.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
FV term k (tm_abs τ t) [=] FV typ k τ ∪ FV term k t
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
FV term k (tm_abs τ t) [=] FV typ k τ ∪ FV term k t
    test_simplification_with_atoms.
  Qed.

  Lemma FV_term_rw2 : forall (τ : typ LN) (t : term LN),
      FV term k (tm_abs τ t) [=]
        FV typ k τ ∪ FV term k t.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
FV term k (tm_abs τ t) [=] FV typ k τ ∪ FV term k t
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
FV term k (tm_abs τ t) [=] FV typ k τ ∪ FV term k t
    test_simplification_with_atoms.
  Qed.

  Lemma FV_term_rw3 : forall (t1 t2 : term LN),
      FV term k (tm_app t1 t2) [=]
        FV term k t1 ∪ FV term k t2.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : term LN,
FV term k (tm_app t1 t2)
[=] FV term k t1 ∪ FV term k t2
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t1 t2 : term LN,
FV term k (tm_app t1 t2)
[=] FV term k t1 ∪ FV term k t2
    test_simplification_with_atoms.
  Qed.

  Lemma FV_term_rw4 : forall (t : term LN),
      FV term k (tm_tab t) [=]
        FV term k t.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t : term LN,
FV term k (tm_tab t) [=] FV term k t
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall t : term LN,
FV term k (tm_tab t) [=] FV term k t
    test_simplification_with_atoms.
  Qed.

  Lemma FV_term_rw5 : forall (t: term LN) (τ : typ LN),
      FV term k (tm_tap t τ) [=]
        FV term k t ∪ FV typ k τ.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (t : term LN) (τ : typ LN),
FV term k (tm_tap t τ) [=] FV term k t ∪ FV typ k τ
  Proof.A: Type
k: K2
n: nat
x: atom
u: SystemF k LN
forall (t : term LN) (τ : typ LN),
FV term k (tm_tap t τ) [=] FV term k t ∪ FV typ k τ
    test_simplification_with_atoms.
  Qed.

End rw_FV.

Ltac simplify_scoped_pre_refold_hook :=
  idtac.

Ltac simplify_scoped_post_refold_hook :=
  idtac.

Ltac simplify_scoped :=
  match goal with
  | |- context[scoped (T := ?T) (ix := ?ix)
                ?U ?k ?n ?t] =>
      idtac
  end.
(*
      rewrite ?(scoped_to_Forallkd _(*U*) (ix := ix));
      simplify_Forallkd;
      simplify_scoped_pre_refold_hook;
      rewrite <- ?(scoped_to_Forallkd _ (ix := ix));
      simplify_scoped_post_refold_hook
*)

(** ** <<scoped>> *)
(******************************************************************************)
Section rw_scoped.

  Context
    (A : Type)
      (k : K2)
      (Γ : AtomSet.t)
      (u: SystemF k LN).

  Ltac tactic_being_tested ::= simplify_scoped.

  Lemma scoped_type_rw1 : forall c,
      scoped typ k (ty_c c) Γ <-> True.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall c : base_typ, scoped typ k (ty_c c) Γ <-> True
  Proof.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall c : base_typ, scoped typ k (ty_c c) Γ <-> True
    intros.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
c: base_typ
scoped typ k (ty_c c) Γ <-> True
    unfold scoped.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
c: base_typ
FV typ k (ty_c c) ⊆ Γ <-> True
    simplify_FV.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
c: base_typ
∅%set ⊆ Γ <-> True
    split; fsetdec.
  Qed.

  (*
  Lemma scoped_type_rw2_neq : forall (a : A),
      k <> ktyp ->
      LC typ k f (ty_v a) = ty_v a.
  Proof.
    intros.
    simplify_LC.
    rewrite btgd_neq; auto.
  Qed.*)

  Lemma scoped_type_rw3 : forall (t1 t2 : typ LN),
      scoped typ k (ty_ar t1 t2) Γ <->
        (scoped typ k t1 Γ /\ scoped typ k t2 Γ).A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall t1 t2 : typ LN,
scoped typ k (ty_ar t1 t2) Γ <->
scoped typ k t1 Γ /\ scoped typ k t2 Γ
  Proof.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall t1 t2 : typ LN,
scoped typ k (ty_ar t1 t2) Γ <->
scoped typ k t1 Γ /\ scoped typ k t2 Γ
    intros.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t1, t2: typ LN
scoped typ k (ty_ar t1 t2) Γ <->
scoped typ k t1 Γ /\ scoped typ k t2 Γ
    unfold scoped.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t1, t2: typ LN
FV typ k (ty_ar t1 t2) ⊆ Γ <->
FV typ k t1 ⊆ Γ /\ FV typ k t2 ⊆ Γ
    simplify_FV.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t1, t2: typ LN
(FV typ k t1 ∪ FV typ k t2)%set ⊆ Γ <->
FV typ k t1 ⊆ Γ /\ FV typ k t2 ⊆ Γ
    intuition fsetdec.
  Qed.

  Lemma scoped_type_rw4_eq : forall (body : typ LN),
      scoped typ k (ty_univ body) Γ <->
        scoped typ k body Γ.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall body : typ LN,
scoped typ k (ty_univ body) Γ <-> scoped typ k body Γ
  Proof.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall body : typ LN,
scoped typ k (ty_univ body) Γ <-> scoped typ k body Γ
    intros.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
body: typ LN
scoped typ k (ty_univ body) Γ <-> scoped typ k body Γ
    unfold scoped.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
body: typ LN
FV typ k (ty_univ body) ⊆ Γ <-> FV typ k body ⊆ Γ
    simplify_FV.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
body: typ LN
FV typ k body ⊆ Γ <-> FV typ k body ⊆ Γ
    intuition fsetdec.
  Qed.

  Lemma scoped_type_rw4_neq : forall (body : typ LN),
      scoped typ k (ty_univ body) =
        scoped typ k body.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall body : typ LN,
scoped typ k (ty_univ body) = scoped typ k body
  Proof.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall body : typ LN,
scoped typ k (ty_univ body) = scoped typ k body
    intros.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
body: typ LN
scoped typ k (ty_univ body) = scoped typ k body
    unfold scoped.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
body: typ LN
(fun γ : AtomSet.t => FV typ k (ty_univ body) ⊆ γ) =
(fun γ : AtomSet.t => FV typ k body ⊆ γ)
    simplify_FV.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
body: typ LN
(fun γ : AtomSet.t => FV typ k body ⊆ γ) =
(fun γ : AtomSet.t => FV typ k body ⊆ γ)
    conclude.
  Qed.

  #[local] Open Scope set_scope.

  Lemma scoped_term_rw1_eq : forall (x : atom),
      k = ktrm ->
      scoped term k (tm_var (Fr x)) Γ = ({{x}} ⊆ Γ).A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall x : atom,
k = ktrm ->
scoped term k (tm_var (Fr x)) Γ = ({{x}} ⊆ Γ)
  Proof.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall x : atom,
k = ktrm ->
scoped term k (tm_var (Fr x)) Γ = ({{x}} ⊆ Γ)
    intros.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
x: atom
H: k = ktrm
scoped term k (tm_var (Fr x)) Γ = ({{x}} ⊆ Γ)
    unfold scoped.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
x: atom
H: k = ktrm
(FV term k (tm_var (Fr x)) ⊆ Γ) = ({{x}} ⊆ Γ)
    simplify_FV.
  Qed.

  Lemma scoped_term_rw1_neq : forall (x : atom),
      k <> ktrm ->
      scoped term k (tm_var (Fr x)) Γ = True.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall x : atom,
k <> ktrm -> scoped term k (tm_var (Fr x)) Γ = True
  Proof.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall x : atom,
k <> ktrm -> scoped term k (tm_var (Fr x)) Γ = True
    intros.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
x: atom
H: k <> ktrm
scoped term k (tm_var (Fr x)) Γ = True
    unfold scoped.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
x: atom
H: k <> ktrm
(FV term k (tm_var (Fr x)) ⊆ Γ) = True
    propext; simplify_FV.
  Qed.

  Lemma scoped_term_rw2: forall (τ : typ LN) (t : term LN),
      scoped term k (tm_abs τ t) Γ <->
        (scoped typ k τ Γ /\ scoped term k t Γ).A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
scoped term k (tm_abs τ t) Γ <->
scoped typ k τ Γ /\ scoped term k t Γ
  Proof.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall (τ : typ LN) (t : term LN),
scoped term k (tm_abs τ t) Γ <->
scoped typ k τ Γ /\ scoped term k t Γ
    intros.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
τ: typ LN
t: term LN
scoped term k (tm_abs τ t) Γ <->
scoped typ k τ Γ /\ scoped term k t Γ
    unfold scoped.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
τ: typ LN
t: term LN
FV term k (tm_abs τ t) ⊆ Γ <->
FV typ k τ ⊆ Γ /\ FV term k t ⊆ Γ
    simplify_FV.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
τ: typ LN
t: term LN
FV typ k τ ∪ FV term k t ⊆ Γ <->
FV typ k τ ⊆ Γ /\ FV term k t ⊆ Γ
    intuition fsetdec.
  Qed.

  Lemma scoped_term_rw3 : forall (t1 t2 : term LN),
      scoped term k (tm_app t1 t2) Γ <->
        (scoped term k t1 Γ /\ scoped term k t2 Γ).A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall t1 t2 : term LN,
scoped term k (tm_app t1 t2) Γ <->
scoped term k t1 Γ /\ scoped term k t2 Γ
  Proof.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall t1 t2 : term LN,
scoped term k (tm_app t1 t2) Γ <->
scoped term k t1 Γ /\ scoped term k t2 Γ
    intros.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t1, t2: term LN
scoped term k (tm_app t1 t2) Γ <->
scoped term k t1 Γ /\ scoped term k t2 Γ
    unfold scoped.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t1, t2: term LN
FV term k (tm_app t1 t2) ⊆ Γ <->
FV term k t1 ⊆ Γ /\ FV term k t2 ⊆ Γ
    simplify_FV.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t1, t2: term LN
FV term k t1 ∪ FV term k t2 ⊆ Γ <->
FV term k t1 ⊆ Γ /\ FV term k t2 ⊆ Γ
    intuition fsetdec.
  Qed.

  Lemma scoped_term_rw4_neq : forall (t : term LN),
      scoped term k (tm_tab t) Γ <->
        scoped term k t Γ.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall t : term LN,
scoped term k (tm_tab t) Γ <-> scoped term k t Γ
  Proof.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall t : term LN,
scoped term k (tm_tab t) Γ <-> scoped term k t Γ
    intros.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t: term LN
scoped term k (tm_tab t) Γ <-> scoped term k t Γ
    unfold scoped.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t: term LN
FV term k (tm_tab t) ⊆ Γ <-> FV term k t ⊆ Γ
    simplify_FV.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t: term LN
FV term k t ⊆ Γ <-> FV term k t ⊆ Γ
    intuition fsetdec.
  Qed.

  Lemma scoped_term_rw4_eq : forall (t : term LN),
      scoped term k (tm_tab t) Γ <->
        scoped term k t Γ.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall t : term LN,
scoped term k (tm_tab t) Γ <-> scoped term k t Γ
  Proof.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall t : term LN,
scoped term k (tm_tab t) Γ <-> scoped term k t Γ
    intros.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t: term LN
scoped term k (tm_tab t) Γ <-> scoped term k t Γ
    unfold scoped.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t: term LN
FV term k (tm_tab t) ⊆ Γ <-> FV term k t ⊆ Γ
    simplify_FV.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t: term LN
FV term k t ⊆ Γ <-> FV term k t ⊆ Γ
    intuition fsetdec.
  Qed.

  Lemma scoped_term_rw5 : forall (t: term LN) (τ : typ LN),
      scoped term k (tm_tap t τ) Γ <->
        (scoped term k t Γ /\ scoped typ k τ Γ).A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall (t : term LN) (τ : typ LN),
scoped term k (tm_tap t τ) Γ <->
scoped term k t Γ /\ scoped typ k τ Γ
  Proof.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
forall (t : term LN) (τ : typ LN),
scoped term k (tm_tap t τ) Γ <->
scoped term k t Γ /\ scoped typ k τ Γ
    intros.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t: term LN
τ: typ LN
scoped term k (tm_tap t τ) Γ <->
scoped term k t Γ /\ scoped typ k τ Γ
    unfold scoped.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t: term LN
τ: typ LN
FV term k (tm_tap t τ) ⊆ Γ <->
FV term k t ⊆ Γ /\ FV typ k τ ⊆ Γ
    simplify_FV.A: Type
k: K2
Γ: AtomSet.t
u: SystemF k LN
t: term LN
τ: typ LN
FV term k t ∪ FV typ k τ ⊆ Γ <->
FV term k t ⊆ Γ /\ FV typ k τ ⊆ Γ
    intuition fsetdec.
  Qed.

End rw_scoped.