From Tealeaves Require Export
  Examples.SystemF.Syntax
  Simplification.Tests.Support
  Simplification.MBinddt
  Simplification.Tests.SystemF_Binddt.

#[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 M.

Section local_lemmas_needed.

  Context
    (U : Type -> Type)
      `{MultiDecoratedTraversablePreModule W T U}
      `{! MultiDecoratedTraversableMonad W T}.

  Lemma kbindd_to_mbindd: forall A (k: K) (f: W * A -> T k A),
      kbindd U k f =  mbindd U (btgd k f).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (k : K) (f : W * A -> T k A),
kbindd U k f = mbindd U (btgd k f)
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (k : K) (f : W * A -> T k A),
kbindd U k f = mbindd U (btgd k f)
    reflexivity.
  Qed.

  Lemma kbind_to_mbind: forall A (k: K) (f: A -> T k A),
      kbind U k f =  mbind U (btg k f).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (k : K) (f : A -> T k A),
kbind U k f = mbind U (btg k f)
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (k : K) (f : A -> T k A),
kbind U k f = mbind U (btg k f)
    reflexivity.
  Qed.

  Lemma btgd_compose_incr: forall A (k: K) (f: W * A -> SystemF k A) w,
      btgd k f ◻ allK (incr w) =
        btgd k (f ⦿ w).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (k : K) (f : W * A -> SystemF k A)
  (w : W), btgd k f ◻ allK (incr w) = btgd k (f ⦿ w)
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (k : K) (f : W * A -> SystemF k A)
  (w : W), btgd k f ◻ allK (incr w) = btgd k (f ⦿ w)
    intros.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
k: K
f: W * A -> SystemF k A
w: W
btgd k f ◻ allK (incr w) = btgd k (f ⦿ w)
    ext j.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
k: K
f: W * A -> SystemF k A
w: W
j: K
(btgd k f ◻ allK (incr w)) j = btgd k (f ⦿ w) j
    unfold allK, const.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
k: K
f: W * A -> SystemF k A
w: W
j: K
(btgd k f ◻ (fun _ : K => incr w)) j =
btgd k (f ⦿ w) j
    unfold vec_compose.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
k: K
f: W * A -> SystemF k A
w: W
j: K
btgd k f j ∘ incr w = btgd k (f ⦿ w) j
    compare values k and j.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
j: K
f: W * A -> SystemF j A
w: W
DESTR_EQs: j = j
btgd j f j ∘ incr w = btgd j (f ⦿ w) j
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
k: K
f: W * A -> SystemF k A
w: W
j: K
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
btgd k f j ∘ incr w = btgd k (f ⦿ w) j
    {
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
j: K
f: W * A -> SystemF j A
w: W
DESTR_EQs: j = j
btgd j f j ∘ incr w = btgd j (f ⦿ w) j autorewrite with tea_tgt_eq.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
j: K
f: W * A -> SystemF j A
w: W
DESTR_EQs: j = j
f ∘ incr w = f ⦿ w
      reflexivity. }
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
k: K
f: W * A -> SystemF k A
w: W
j: K
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
btgd k f j ∘ incr w = btgd k (f ⦿ w) j
    {
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
k: K
f: W * A -> SystemF k A
w: W
j: K
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
btgd k f j ∘ incr w = btgd k (f ⦿ w) j autorewrite with tea_tgt_neq.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
k: K
f: W * A -> SystemF k A
w: W
j: K
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
mret SystemF j ∘ extract ∘ incr w =
mret SystemF j ∘ extract
      reassociate -> on left.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
k: K
f: W * A -> SystemF k A
w: W
j: K
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
mret SystemF j ∘ (extract ∘ incr w) =
mret SystemF j ∘ extract
      rewrite extract_incr.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
k: K
f: W * A -> SystemF k A
w: W
j: K
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
mret SystemF j ∘ extract = mret SystemF j ∘ extract
      reflexivity. }
  Qed.

  Lemma tgtdt_compose_incr `{Applicative G}:
    forall A (k: K) (f: W * A -> G A) w,
      tgtdt k f ◻ allK (incr w) =
        tgtdt k (f ⦿ w).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
forall (A : Type) (k : K) (f : W * A -> G A) (w : W),
tgtdt k f ◻ allK (incr w) = tgtdt k (f ⦿ w)
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
forall (A : Type) (k : K) (f : W * A -> G A) (w : W),
tgtdt k f ◻ allK (incr w) = tgtdt k (f ⦿ w)
    intros.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
k: K
f: W * A -> G A
w: W
tgtdt k f ◻ allK (incr w) = tgtdt k (f ⦿ w)
    ext j.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
k: K
f: W * A -> G A
w: W
j: K
(tgtdt k f ◻ allK (incr w)) j = tgtdt k (f ⦿ w) j
    unfold allK, const.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
k: K
f: W * A -> G A
w: W
j: K
(tgtdt k f ◻ (fun _ : K => incr w)) j =
tgtdt k (f ⦿ w) j
    unfold vec_compose, compose.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
k: K
f: W * A -> G A
w: W
j: K
tgtdt k f j ○ incr w = tgtdt k (f ⦿ w) j
    unfold tgtdt.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
k: K
f: W * A -> G A
w: W
j: K
(fun a : W * A =>
 let
 '(w, a0) := incr w a in
  if k == j then f (w, a0) else pure a0) =
(fun '(w0, a) =>
 if k == j then (f ⦿ w) (w0, a) else pure a)
    ext [w' a].
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
k: K
f: W * A -> G A
w: W
j: K
w': W
a: A
(let
 '(w, a) := incr w (w', a) in
  if k == j then f (w, a) else pure a) =
(if k == j then (f ⦿ w) (w', a) else pure a)
    compare values k and j.
  Qed.

End local_lemmas_needed.

Ltac simplify_kbindd_pre_refold_hook :=
  rewrite ?(btgd_compose_incr).

Ltac simplify_kbindd_post_refold_hook :=
  idtac.

Ltac simplify_kbindd :=
  rewrite ?kbindd_to_mbindd;
  simplify_mbindd;
   simplify_kbindd_pre_refold_hook;
  rewrite <- ?kbindd_to_mbindd;
  simplify_kbindd_post_refold_hook.

(** ** <<kbindd>> *)
(******************************************************************************)
Section rw_kbindd.

  Context
    (A : Type)
      (k : K2)
      (f : list K2 * A -> SystemF k A).

  Ltac tactic_being_tested ::= simplify_kbindd.

  Lemma kbindd_type_rw1 : forall c,
      kbindd typ k f (ty_c c) = ty_c c.
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall c : base_typ, kbindd typ k f (ty_c c) = ty_c c
  Proof.
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall c : base_typ, kbindd typ k f (ty_c c) = ty_c c
    test_simplification.
  Qed.

  Lemma kbindd_type_rw2_neq : forall (a : A),
      k <> ktyp ->
      kbindd typ k f (ty_v a) = ty_v a.
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall a : A,
k <> ktyp -> kbindd typ k f (ty_v a) = ty_v a
  Proof.
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall a : A,
k <> ktyp -> kbindd typ k f (ty_v a) = ty_v a
    intros.
A: Type
k: K2
f: list K2 * A -> SystemF k A
a: A
H: k <> ktyp
kbindd typ k f (ty_v a) = ty_v a
    simplify_kbindd.
A: Type
k: K2
f: list K2 * A -> SystemF k A
a: A
H: k <> ktyp
btgd k f ktyp ([], a) = ty_v a
    rewrite btgd_neq; auto.
  Qed.

  (*
    Lemma kbindd_type_neq_rw2_eq : forall (a : A) (Heq: k = ktyp),
        kbindd typ k f (ty_v a) = rew Heq in (f ([], a)).
    Proof.
      intros.
      simplify_kbindd.
      subst.
      rewrite btgd_eq. auto.
    Qed.
   *)

  Lemma kbindd_type_rw3 : forall (t1 t2 : typ A),
      kbindd typ k f (ty_ar t1 t2) =
        ty_ar (kbindd typ k f t1) (kbindd typ k f t2).
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall t1 t2 : typ A,
kbindd typ k f (ty_ar t1 t2) =
ty_ar (kbindd typ k f t1) (kbindd typ k f t2)
  Proof.
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall t1 t2 : typ A,
kbindd typ k f (ty_ar t1 t2) =
ty_ar (kbindd typ k f t1) (kbindd typ k f t2)
    test_simplification.
  Qed.

  Lemma kbindd_type_rw4 : forall (body : typ A),
      kbindd typ k f (ty_univ body) =
        ty_univ (kbindd typ k (f ⦿ [ktyp]) body).
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall body : typ A,
kbindd typ k f (ty_univ body) =
ty_univ (kbindd typ k (f ⦿ [ktyp]) body)
  Proof.
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall body : typ A,
kbindd typ k f (ty_univ body) =
ty_univ (kbindd typ k (f ⦿ [ktyp]) body)
    test_simplification.
  Qed.

  Lemma kbindd_term_rw1_neq : forall (a : A),
      k <> ktrm ->
      kbindd term k f (tm_var a) = tm_var a.
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall a : A,
k <> ktrm -> kbindd term k f (tm_var a) = tm_var a
  Proof.
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall a : A,
k <> ktrm -> kbindd term k f (tm_var a) = tm_var a
    intros.
A: Type
k: K2
f: list K2 * A -> SystemF k A
a: A
H: k <> ktrm
kbindd term k f (tm_var a) = tm_var a
    simplify_kbindd.
A: Type
k: K2
f: list K2 * A -> SystemF k A
a: A
H: k <> ktrm
btgd k f ktrm ([], a) = tm_var a
    rewrite btgd_neq; auto.
  Qed.

  Lemma kbindd_term_rw2 : forall (τ : typ A) (t : term A),
      kbindd term k f (tm_abs τ t) =
        tm_abs (kbindd typ k f τ) (kbindd term k (f ⦿ [ktrm]) t).
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall (τ : typ A) (t : term A),
kbindd term k f (tm_abs τ t) =
tm_abs (kbindd typ k f τ)
  (kbindd term k (f ⦿ [ktrm]) t)
  Proof.
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall (τ : typ A) (t : term A),
kbindd term k f (tm_abs τ t) =
tm_abs (kbindd typ k f τ)
  (kbindd term k (f ⦿ [ktrm]) t)
    test_simplification.
  Qed.

  Lemma kbindd_term_rw3 : forall (t1 t2 : term A),
      kbindd term k f (tm_app t1 t2) =
        tm_app (kbindd term k f t1) (kbindd term k f t2).
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall t1 t2 : term A,
kbindd term k f (tm_app t1 t2) =
tm_app (kbindd term k f t1) (kbindd term k f t2)
  Proof.
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall t1 t2 : term A,
kbindd term k f (tm_app t1 t2) =
tm_app (kbindd term k f t1) (kbindd term k f t2)
    test_simplification.
  Qed.

  Lemma kbindd_term_rw4 : forall (t : term A),
      kbindd term k f (tm_tab t) =
        tm_tab (kbindd term k (f ⦿ [ktyp]) t).
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall t : term A,
kbindd term k f (tm_tab t) =
tm_tab (kbindd term k (f ⦿ [ktyp]) t)
  Proof.
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall t : term A,
kbindd term k f (tm_tab t) =
tm_tab (kbindd term k (f ⦿ [ktyp]) t)
    test_simplification.
  Qed.

  Lemma kbindd_term_rw5 : forall (t: term A) (τ : typ A),
      kbindd term k f (tm_tap t τ) =
        tm_tap (kbindd term k f t) (kbindd typ k f τ).
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall (t : term A) (τ : typ A),
kbindd term k f (tm_tap t τ) =
tm_tap (kbindd term k f t) (kbindd typ k f τ)
  Proof.
A: Type
k: K2
f: list K2 * A -> SystemF k A
forall (t : term A) (τ : typ A),
kbindd term k f (tm_tap t τ) =
tm_tap (kbindd term k f t) (kbindd typ k f τ)
    test_simplification.
  Qed.

End rw_kbindd.

Ltac simplify_kbind_pre_refold_hook :=
  rewrite ?(btgd_compose_incr).

Ltac simplify_kbind_post_refold_hook :=
  idtac.

Ltac simplify_kbind :=
  rewrite ?kbind_to_mbind;
  simplify_mbind;
  simplify_kbind_pre_refold_hook;
  rewrite <- ?kbind_to_mbind;
  simplify_kbind_post_refold_hook.

(** ** <<kbind>> *)
(******************************************************************************)
Section rw_kbind.

  Context
    (A : Type)
      (k : K2)
      (f : A -> SystemF k A).
  Ltac tactic_being_tested ::= simplify_kbind.

  Lemma kbind_type_rw1 : forall c,
      kbind typ k f (ty_c c) = ty_c c.
A: Type
k: K2
f: A -> SystemF k A
forall c : base_typ, kbind typ k f (ty_c c) = ty_c c
  Proof.
A: Type
k: K2
f: A -> SystemF k A
forall c : base_typ, kbind typ k f (ty_c c) = ty_c c
    test_simplification.
  Qed.

  Lemma kbind_type_rw2_neq : forall (a : A),
      k <> ktyp ->
      kbind typ k f (ty_v a) = ty_v a.
A: Type
k: K2
f: A -> SystemF k A
forall a : A,
k <> ktyp -> kbind typ k f (ty_v a) = ty_v a
  Proof.
A: Type
k: K2
f: A -> SystemF k A
forall a : A,
k <> ktyp -> kbind typ k f (ty_v a) = ty_v a
    intros.
A: Type
k: K2
f: A -> SystemF k A
a: A
H: k <> ktyp
kbind typ k f (ty_v a) = ty_v a
    rewrite ?kbind_to_mbind;
  simplify_mbind;
  simplify_kbind_pre_refold_hook;
  rewrite <- ?kbind_to_mbind;
  simplify_kbind_post_refold_hook.
A: Type
k: K2
f: A -> SystemF k A
a: A
H: k <> ktyp
btg k f ktyp a = ty_v a
    try rewrite btg_neq; auto.
  Abort.

  Lemma kbind_type_rw3 : forall (t1 t2 : typ A),
      kbind typ k f (ty_ar t1 t2) =
        ty_ar (kbind typ k f t1) (kbind typ k f t2).
A: Type
k: K2
f: A -> SystemF k A
forall t1 t2 : typ A,
kbind typ k f (ty_ar t1 t2) =
ty_ar (kbind typ k f t1) (kbind typ k f t2)
  Proof.
A: Type
k: K2
f: A -> SystemF k A
forall t1 t2 : typ A,
kbind typ k f (ty_ar t1 t2) =
ty_ar (kbind typ k f t1) (kbind typ k f t2)
    test_simplification.
  Qed.

  Lemma kbind_type_rw4 : forall (body : typ A),
      kbind typ k f (ty_univ body) =
        ty_univ (kbind typ k f body).
A: Type
k: K2
f: A -> SystemF k A
forall body : typ A,
kbind typ k f (ty_univ body) =
ty_univ (kbind typ k f body)
  Proof.
A: Type
k: K2
f: A -> SystemF k A
forall body : typ A,
kbind typ k f (ty_univ body) =
ty_univ (kbind typ k f body)
    test_simplification.
  Qed.

  Lemma kbind_term_rw1_neq : forall (a : A),
      k <> ktrm ->
      kbind term k f (tm_var a) = tm_var a.
A: Type
k: K2
f: A -> SystemF k A
forall a : A,
k <> ktrm -> kbind term k f (tm_var a) = tm_var a
  Proof.
A: Type
k: K2
f: A -> SystemF k A
forall a : A,
k <> ktrm -> kbind term k f (tm_var a) = tm_var a
    intros.
A: Type
k: K2
f: A -> SystemF k A
a: A
H: k <> ktrm
kbind term k f (tm_var a) = tm_var a
    simplify_kbind.
A: Type
k: K2
f: A -> SystemF k A
a: A
H: k <> ktrm
btg k f ktrm a = tm_var a
    try rewrite btg_neq; auto.
  Abort.

  Lemma kbind_term_rw2 : forall (τ : typ A) (t : term A),
      kbind term k f (tm_abs τ t) =
        tm_abs (kbind typ k f τ) (kbind term k f t).
A: Type
k: K2
f: A -> SystemF k A
forall (τ : typ A) (t : term A),
kbind term k f (tm_abs τ t) =
tm_abs (kbind typ k f τ) (kbind term k f t)
  Proof.
A: Type
k: K2
f: A -> SystemF k A
forall (τ : typ A) (t : term A),
kbind term k f (tm_abs τ t) =
tm_abs (kbind typ k f τ) (kbind term k f t)
    test_simplification.
  Qed.

  Lemma kbind_term_rw3 : forall (t1 t2 : term A),
      kbind term k f (tm_app t1 t2) =
        tm_app (kbind term k f t1) (kbind term k f t2).
A: Type
k: K2
f: A -> SystemF k A
forall t1 t2 : term A,
kbind term k f (tm_app t1 t2) =
tm_app (kbind term k f t1) (kbind term k f t2)
  Proof.
A: Type
k: K2
f: A -> SystemF k A
forall t1 t2 : term A,
kbind term k f (tm_app t1 t2) =
tm_app (kbind term k f t1) (kbind term k f t2)
    test_simplification.
  Qed.

  Lemma kbind_term_rw4 : forall (t : term A),
      kbind term k f (tm_tab t) =
        tm_tab (kbind term k f t).
A: Type
k: K2
f: A -> SystemF k A
forall t : term A,
kbind term k f (tm_tab t) = tm_tab (kbind term k f t)
  Proof.
A: Type
k: K2
f: A -> SystemF k A
forall t : term A,
kbind term k f (tm_tab t) = tm_tab (kbind term k f t)
    test_simplification.
  Qed.

  Lemma kbind_term_rw5 : forall (t: term A) (τ : typ A),
      kbind term k f (tm_tap t τ) =
        tm_tap (kbind term k f t) (kbind typ k f τ).
A: Type
k: K2
f: A -> SystemF k A
forall (t : term A) (τ : typ A),
kbind term k f (tm_tap t τ) =
tm_tap (kbind term k f t) (kbind typ k f τ)
  Proof.
A: Type
k: K2
f: A -> SystemF k A
forall (t : term A) (τ : typ A),
kbind term k f (tm_tap t τ) =
tm_tap (kbind term k f t) (kbind typ k f τ)
    test_simplification.
  Qed.

End rw_kbind.

Ltac simplify_kmapdt_pre_refold_hook ix :=
  rewrite ?(tgtdt_compose_incr (ix := ix)).

Ltac simplify_kmapdt_post_refold_hook :=
  idtac.

Ltac simplify_kmapdt :=
  match goal with
  | |- context[kmapdt (W := ?W) (T := ?T) (ix := ?ix)
                ?U ?k ?f ?t] =>
      rewrite ?kmapdt_to_mmapdt;
      simplify_mmapdt;
      simplify_kmapdt_pre_refold_hook ix;
      rewrite <- ?kmapdt_to_mmapdt;
      simplify_kmapdt_post_refold_hook
  end.

(** ** <<kmapdt>> *)
(******************************************************************************)
Section rw_kmapdt.

  Context
    (A : Type)
      `{Applicative G}
      (k : K2)
      (f : list K2 * A -> G A).

  Ltac tactic_being_tested ::= simplify_kmapdt.

  Lemma kmapdt_type_rw1 : forall c,
      kmapdt (G := G) typ k f (ty_c c) = pure (F := G) (ty_c c).
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall c : base_typ,
kmapdt typ k f (ty_c c) = pure (ty_c c)
  Proof.
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall c : base_typ,
kmapdt typ k f (ty_c c) = pure (ty_c c)
    test_simplification.
  Qed.

  Lemma kmapdt_type_rw2_neq : forall (a : A),
      k <> ktyp ->
      kmapdt typ k f (ty_v a) = pure (ty_v a).
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall a : A,
k <> ktyp -> kmapdt typ k f (ty_v a) = pure (ty_v a)
  Proof.
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall a : A,
k <> ktyp -> kmapdt typ k f (ty_v a) = pure (ty_v a)
    intros.
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
a: A
H0: k <> ktyp
kmapdt typ k f (ty_v a) = pure (ty_v a)
    simplify_kmapdt.
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
a: A
H0: k <> ktyp
pure (mret SystemF ktyp) <⋆> tgtdt k f ktyp ([], a) =
pure (ty_v a)
  Abort.

  (*
    Lemma kmapdt_type_neq_rw2_eq : forall (a : A) (Heq: k = ktyp),
        kmapdt typ k f (ty_v a) = rew Heq in (f ([], a)).
    Proof.
      intros.
      simplify_kmapdt.
      subst.
      rewrite btgd_eq. auto.
    Qed.
   *)

  Lemma kmapdt_type_rw3 : forall (t1 t2 : typ A),
      kmapdt typ k f (ty_ar t1 t2) =
        pure ty_ar <⋆> (kmapdt typ k f t1) <⋆> (kmapdt typ k f t2).
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall t1 t2 : typ A,
kmapdt typ k f (ty_ar t1 t2) =
pure ty_ar <⋆> kmapdt typ k f t1 <⋆> kmapdt typ k f t2
  Proof.
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall t1 t2 : typ A,
kmapdt typ k f (ty_ar t1 t2) =
pure ty_ar <⋆> kmapdt typ k f t1 <⋆> kmapdt typ k f t2
    test_simplification.
  Qed.

  Lemma kmapdt_type_rw4 : forall (body : typ A),
      kmapdt typ k f (ty_univ body) =
        pure ty_univ <⋆> (kmapdt typ k (f ⦿ [ktyp]) body).
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall body : typ A,
kmapdt typ k f (ty_univ body) =
pure ty_univ <⋆> kmapdt typ k (f ⦿ [ktyp]) body
  Proof.
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall body : typ A,
kmapdt typ k f (ty_univ body) =
pure ty_univ <⋆> kmapdt typ k (f ⦿ [ktyp]) body
    test_simplification.
  Qed.

  (*
  Lemma kmapdt_term_rw1_neq : forall (a : A),
      k <> ktrm ->
      kmapdt term k f (tm_var a) = tm_var a.
  Proof.
    intros.
    simplify_kmapdt.
    rewrite btgd_neq; auto.
  Qed.
  *)

  Lemma kmapdt_term_rw2 : forall (τ : typ A) (t : term A),
      kmapdt term k f (tm_abs τ t) =
        pure tm_abs <⋆> (kmapdt typ k f τ)
          <⋆> (kmapdt term k (f ⦿ [ktrm]) t).
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall (τ : typ A) (t : term A),
kmapdt term k f (tm_abs τ t) =
pure tm_abs <⋆> kmapdt typ k f τ <⋆>
kmapdt term k (f ⦿ [ktrm]) t
  Proof.
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall (τ : typ A) (t : term A),
kmapdt term k f (tm_abs τ t) =
pure tm_abs <⋆> kmapdt typ k f τ <⋆>
kmapdt term k (f ⦿ [ktrm]) t
    test_simplification.
  Qed.

  Lemma kmapdt_term_rw3 : forall (t1 t2 : term A),
      kmapdt term k f (tm_app t1 t2) =
        pure tm_app <⋆> (kmapdt term k f t1)
          <⋆> (kmapdt term k f t2).
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall t1 t2 : term A,
kmapdt term k f (tm_app t1 t2) =
pure tm_app <⋆> kmapdt term k f t1 <⋆>
kmapdt term k f t2
  Proof.
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall t1 t2 : term A,
kmapdt term k f (tm_app t1 t2) =
pure tm_app <⋆> kmapdt term k f t1 <⋆>
kmapdt term k f t2
    test_simplification.
  Qed.

  Lemma kmapdt_term_rw4 : forall (t : term A),
      kmapdt term k f (tm_tab t) =
        pure tm_tab <⋆> (kmapdt term k (f ⦿ [ktyp]) t).
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall t : term A,
kmapdt term k f (tm_tab t) =
pure tm_tab <⋆> kmapdt term k (f ⦿ [ktyp]) t
  Proof.
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall t : term A,
kmapdt term k f (tm_tab t) =
pure tm_tab <⋆> kmapdt term k (f ⦿ [ktyp]) t
    test_simplification.
  Qed.

  Lemma kmapdt_term_rw5 : forall (t: term A) (τ : typ A),
      kmapdt term k f (tm_tap t τ) =
        pure tm_tap <⋆> (kmapdt term k f t) <⋆> (kmapdt typ k f τ).
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall (t : term A) (τ : typ A),
kmapdt term k f (tm_tap t τ) =
pure tm_tap <⋆> kmapdt term k f t <⋆> kmapdt typ k f τ
  Proof.
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
k: K2
f: list K2 * A -> G A
forall (t : term A) (τ : typ A),
kmapdt term k f (tm_tap t τ) =
pure tm_tap <⋆> kmapdt term k f t <⋆> kmapdt typ k f τ
    test_simplification.
  Qed.

End rw_kmapdt.

Ltac simplify_mapReducekd_pre_refold_hook ix :=
  idtac.

Ltac simplify_mapReducekd_post_refold_hook M :=
  repeat simplify_applicative_const;
  repeat simplify_monoid_units;
  change (@const Type Type M ?anything) with M.

Ltac simplify_mapReducekd :=
  match goal with
  | |- context[mapReducekd (W := ?W) (T := ?T) (ix := ?ix)
                        (M := ?M)
                ?U ?k ?f ?t] =>
  rewrite ?(mapReducekd_to_kmapdt U (M := M));
  simplify_kmapdt;
  simplify_mapReducekd_pre_refold_hook ix;
  rewrite <- ?(mapReducekd_to_kmapdt U (M := M));
  rewrite <- ?(mapReducekd_to_kmapdt _ (M := M));
  (* ^ This is used because "_" might not match the U *)
  simplify_mapReducekd_post_refold_hook M
  end.

(** ** <<mapReducekd>> *)
(******************************************************************************)
Section rw_mapReducekd.

  Context
    (A : Type)
      `{Monoid M}
      (k : K2)
      (f : list K2 * A -> M).

  Ltac tactic_being_tested ::= simplify_mapReducekd.

  Lemma mapReducekd_type_rw1 : forall c,
      mapReducekd typ k f (ty_c c) = Ƶ.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall c : base_typ, mapReducekd typ k f (ty_c c) = Ƶ
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall c : base_typ, mapReducekd typ k f (ty_c c) = Ƶ
    test_simplification.
  Qed.

  Lemma mapReducekd_type_rw2_neq : forall (a : A),
      k <> ktyp ->
      mapReducekd typ k f (ty_v a) = pure (ty_v a).
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall a : A,
k <> ktyp ->
mapReducekd typ k f (ty_v a) = pure (ty_v a)
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall a : A,
k <> ktyp ->
mapReducekd typ k f (ty_v a) = pure (ty_v a)
    intros.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
a: A
H0: k <> ktyp
mapReducekd typ k f (ty_v a) = pure (ty_v a)
    simplify_mapReducekd.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
a: A
H0: k <> ktyp
(if EqDec_eq_of_EqDec Keq k ktyp then f ([], a) else Ƶ) =
pure (ty_v a)
  Abort.

  (*
    Lemma mapReducekd_type_neq_rw2_eq : forall (a : A) (Heq: k = ktyp),
        mapReducekd typ k f (ty_v a) = rew Heq in (f ([], a)).
    Proof.
      intros.
      simplify_mapReducekd.
      subst.
      rewrite btgd_eq. auto.
    Qed.
   *)

  Lemma mapReducekd_type_rw3 : forall (t1 t2 : typ A),
      mapReducekd typ k f (ty_ar t1 t2) =
        mapReducekd typ k f t1 ● mapReducekd typ k f t2.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall t1 t2 : typ A,
mapReducekd typ k f (ty_ar t1 t2) =
mapReducekd typ k f t1 ● mapReducekd typ k f t2
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall t1 t2 : typ A,
mapReducekd typ k f (ty_ar t1 t2) =
mapReducekd typ k f t1 ● mapReducekd typ k f t2
    test_simplification.
  Qed.

  Lemma mapReducekd_type_rw4 : forall (body : typ A),
      mapReducekd typ k f (ty_univ body) =
        mapReducekd typ k (f ⦿ [ktyp]) body.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall body : typ A,
mapReducekd typ k f (ty_univ body) =
mapReducekd typ k (f ⦿ [ktyp]) body
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall body : typ A,
mapReducekd typ k f (ty_univ body) =
mapReducekd typ k (f ⦿ [ktyp]) body
    test_simplification.
  Qed.

  (*
  Lemma mapReducekd_term_rw1_neq : forall (a : A),
      k <> ktrm ->
      mapReducekd term k f (tm_var a) = tm_var a.
  Proof.
    intros.
    simplify_mapReducekd.
    rewrite btgd_neq; auto.
  Qed.
  *)

  Lemma mapReducekd_term_rw2 : forall (τ : typ A) (t : term A),
      mapReducekd term k f (tm_abs τ t) =
        mapReducekd typ k f τ ● mapReducekd term k (f ⦿ [ktrm]) t.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall (τ : typ A) (t : term A),
mapReducekd term k f (tm_abs τ t) =
mapReducekd typ k f τ
● mapReducekd term k (f ⦿ [ktrm]) t
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall (τ : typ A) (t : term A),
mapReducekd term k f (tm_abs τ t) =
mapReducekd typ k f τ
● mapReducekd term k (f ⦿ [ktrm]) t
    test_simplification.
  Qed.

  Lemma mapReducekd_term_rw3 : forall (t1 t2 : term A),
      mapReducekd term k f (tm_app t1 t2) =
        mapReducekd term k f t1 ● mapReducekd term k f t2.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall t1 t2 : term A,
mapReducekd term k f (tm_app t1 t2) =
mapReducekd term k f t1 ● mapReducekd term k f t2
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall t1 t2 : term A,
mapReducekd term k f (tm_app t1 t2) =
mapReducekd term k f t1 ● mapReducekd term k f t2
    test_simplification.
  Qed.

  Lemma mapReducekd_term_rw4 : forall (t : term A),
      mapReducekd term k f (tm_tab t) =
        mapReducekd term k (f ⦿ [ktyp]) t.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall t : term A,
mapReducekd term k f (tm_tab t) =
mapReducekd term k (f ⦿ [ktyp]) t
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall t : term A,
mapReducekd term k f (tm_tab t) =
mapReducekd term k (f ⦿ [ktyp]) t
    test_simplification.
  Qed.

  Lemma mapReducekd_term_rw5 : forall (t: term A) (τ : typ A),
      mapReducekd term k f (tm_tap t τ) =
        mapReducekd term k f t ● mapReducekd typ k f τ.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall (t : term A) (τ : typ A),
mapReducekd term k f (tm_tap t τ) =
mapReducekd term k f t ● mapReducekd typ k f τ
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> M
forall (t : term A) (τ : typ A),
mapReducekd term k f (tm_tap t τ) =
mapReducekd term k f t ● mapReducekd typ k f τ
    test_simplification.
  Qed.

End rw_mapReducekd.

Ltac simplify_Forallkd_pre_refold_hook :=
  idtac.

Ltac simplify_Forallkd_post_refold_hook :=
  unfold_ops @Monoid_op_and;
  unfold_ops @Monoid_unit_true.

Ltac simplify_Forallkd :=
  match goal with
  | |- context[Forallkd (W := ?W) (T := ?T) (ix := ?ix)
                ?U ?k ?f ?t] =>
  rewrite ?Forallkd_to_mapReducekd;
  simplify_mapReducekd;
  simplify_Forallkd_pre_refold_hook;
  rewrite <- ?Forallkd_to_mapReducekd;
  simplify_Forallkd_post_refold_hook
  end.

(** ** <<Forallkd>> *)
(******************************************************************************)
Section rw_Forallkd.

  Context
    (A : Type)
      `{Monoid M}
      (k : K2)
      (f : list K2 * A -> Prop).

  Ltac tactic_being_tested ::= simplify_Forallkd.

  Lemma Forallkd_type_rw1 : forall c,
      Forallkd typ k f (ty_c c) = Ƶ.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall c : base_typ, Forallkd typ k f (ty_c c) = Ƶ
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall c : base_typ, Forallkd typ k f (ty_c c) = Ƶ
    test_simplification.
  Qed.

  Lemma Forallkd_type_rw2_neq : forall (a : A),
      k <> ktyp ->
      Forallkd typ k f (ty_v a) = True.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall a : A,
k <> ktyp -> Forallkd typ k f (ty_v a) = True
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall a : A,
k <> ktyp -> Forallkd typ k f (ty_v a) = True
    intros.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
a: A
H0: k <> ktyp
Forallkd typ k f (ty_v a) = True
    simplify_Forallkd.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
a: A
H0: k <> ktyp
(if EqDec_eq_of_EqDec Keq k ktyp
 then f ([], a)
 else True) = True
  Abort.

  (*
    Lemma Forallkd_type_neq_rw2_eq : forall (a : A) (Heq: k = ktyp),
        Forallkd typ k f (ty_v a) = rew Heq in (f ([], a)).
    Proof.
      intros.
      simplify_Forallkd.
      subst.
      rewrite btgd_eq. auto.
    Qed.
   *)

  Lemma Forallkd_type_rw3 : forall (t1 t2 : typ A),
      Forallkd typ k f (ty_ar t1 t2) =
        (Forallkd typ k f t1 /\ Forallkd typ k f t2).
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall t1 t2 : typ A,
Forallkd typ k f (ty_ar t1 t2) =
(Forallkd typ k f t1 /\ Forallkd typ k f t2)
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall t1 t2 : typ A,
Forallkd typ k f (ty_ar t1 t2) =
(Forallkd typ k f t1 /\ Forallkd typ k f t2)
    test_simplification.
  Qed.

  Lemma Forallkd_type_rw4 : forall (body : typ A),
      Forallkd typ k f (ty_univ body) =
        Forallkd typ k (f ⦿ [ktyp]) body.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall body : typ A,
Forallkd typ k f (ty_univ body) =
Forallkd typ k (f ⦿ [ktyp]) body
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall body : typ A,
Forallkd typ k f (ty_univ body) =
Forallkd typ k (f ⦿ [ktyp]) body
    test_simplification.
  Qed.

  (*
  Lemma Forallkd_term_rw1_neq : forall (a : A),
      k <> ktrm ->
      Forallkd term k f (tm_var a) = tm_var a.
  Proof.
    intros.
    simplify_Forallkd.
    rewrite btgd_neq; auto.
  Qed.
  *)

  Lemma Forallkd_term_rw2 : forall (τ : typ A) (t : term A),
      Forallkd term k f (tm_abs τ t) =
        (Forallkd typ k f τ /\ Forallkd term k (f ⦿ [ktrm]) t).
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall (τ : typ A) (t : term A),
Forallkd term k f (tm_abs τ t) =
(Forallkd typ k f τ /\ Forallkd term k (f ⦿ [ktrm]) t)
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall (τ : typ A) (t : term A),
Forallkd term k f (tm_abs τ t) =
(Forallkd typ k f τ /\ Forallkd term k (f ⦿ [ktrm]) t)
    test_simplification.
  Qed.

  Lemma Forallkd_term_rw3 : forall (t1 t2 : term A),
      Forallkd term k f (tm_app t1 t2) =
        (Forallkd term k f t1 /\ Forallkd term k f t2).
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall t1 t2 : term A,
Forallkd term k f (tm_app t1 t2) =
(Forallkd term k f t1 /\ Forallkd term k f t2)
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall t1 t2 : term A,
Forallkd term k f (tm_app t1 t2) =
(Forallkd term k f t1 /\ Forallkd term k f t2)
    test_simplification.
  Qed.

  Lemma Forallkd_term_rw4 : forall (t : term A),
      Forallkd term k f (tm_tab t) =
        Forallkd term k (f ⦿ [ktyp]) t.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall t : term A,
Forallkd term k f (tm_tab t) =
Forallkd term k (f ⦿ [ktyp]) t
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall t : term A,
Forallkd term k f (tm_tab t) =
Forallkd term k (f ⦿ [ktyp]) t
    test_simplification.
  Qed.

  Lemma Forallkd_term_rw5 : forall (t: term A) (τ : typ A),
      Forallkd term k f (tm_tap t τ) =
        (Forallkd term k f t /\ Forallkd typ k f τ).
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall (t : term A) (τ : typ A),
Forallkd term k f (tm_tap t τ) =
(Forallkd term k f t /\ Forallkd typ k f τ)
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: list K2 * A -> Prop
forall (t : term A) (τ : typ A),
Forallkd term k f (tm_tap t τ) =
(Forallkd term k f t /\ Forallkd typ k f τ)
    test_simplification.
  Qed.

End rw_Forallkd.


Ltac simplify_mapReducek_pre_refold_hook ix :=
  repeat push_preincr_into_fn.

Ltac simplify_mapReducek_post_refold_hook M :=
  idtac.

Ltac simplify_mapReducek :=
  match goal with
  | |- context[mapReducek (W := ?W) (T := ?T) (ix := ?ix)
                        (M := ?M)
                ?U ?k ?f ?t] =>
  rewrite ?(mapReducek_to_mapReducekd (ix := ix) U (M := M));
  simplify_mapReducekd;
  simplify_mapReducek_pre_refold_hook ix;
  rewrite <- ?(mapReducek_to_mapReducekd _ (M := M));
  simplify_mapReducek_post_refold_hook M
  end.

(** ** <<mapReducek>> *)
(******************************************************************************)
Section rw_mapReducek.

  Context
    (A : Type)
      `{Monoid M}
      (k : K2)
      (f : A -> M).

  Ltac tactic_being_tested ::= simplify_mapReducek.

  Lemma mapReducek_type_rw1 : forall c,
      mapReducek typ k f (ty_c c) = Ƶ.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall c : base_typ, mapReducek typ k f (ty_c c) = Ƶ
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall c : base_typ, mapReducek typ k f (ty_c c) = Ƶ
    test_simplification.
  Qed.

  Lemma mapReducek_type_rw2_neq : forall (a : A),
      k <> ktyp ->
      mapReducek typ k f (ty_v a) = Ƶ.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall a : A,
k <> ktyp -> mapReducek typ k f (ty_v a) = Ƶ
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall a : A,
k <> ktyp -> mapReducek typ k f (ty_v a) = Ƶ
    intros.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
a: A
H0: k <> ktyp
mapReducek typ k f (ty_v a) = Ƶ
    simplify_mapReducek.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
a: A
H0: k <> ktyp
(if EqDec_eq_of_EqDec Keq k ktyp
 then (f ∘ extract) ([], a)
 else Ƶ) = Ƶ
  Abort.

  Lemma mapReducek_type_rw3 : forall (t1 t2 : typ A),
      mapReducek typ k f (ty_ar t1 t2) =
        mapReducek typ k f t1 ● mapReducek typ k f t2.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall t1 t2 : typ A,
mapReducek typ k f (ty_ar t1 t2) =
mapReducek typ k f t1 ● mapReducek typ k f t2
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall t1 t2 : typ A,
mapReducek typ k f (ty_ar t1 t2) =
mapReducek typ k f t1 ● mapReducek typ k f t2
    test_simplification.
  Qed.

  Lemma mapReducek_type_rw4 : forall (body : typ A),
      mapReducek typ k f (ty_univ body) =
        mapReducek typ k f body.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall body : typ A,
mapReducek typ k f (ty_univ body) =
mapReducek typ k f body
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall body : typ A,
mapReducek typ k f (ty_univ body) =
mapReducek typ k f body
    test_simplification.
  Qed.

  Lemma mapReducek_term_rw2 : forall (τ : typ A) (t : term A),
      mapReducek term k f (tm_abs τ t) =
        mapReducek typ k f τ ● mapReducek term k f t.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall (τ : typ A) (t : term A),
mapReducek term k f (tm_abs τ t) =
mapReducek typ k f τ ● mapReducek term k f t
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall (τ : typ A) (t : term A),
mapReducek term k f (tm_abs τ t) =
mapReducek typ k f τ ● mapReducek term k f t
    test_simplification.
  Qed.

  Lemma mapReducek_term_rw3 : forall (t1 t2 : term A),
      mapReducek term k f (tm_app t1 t2) =
        mapReducek term k f t1 ● mapReducek term k f t2.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall t1 t2 : term A,
mapReducek term k f (tm_app t1 t2) =
mapReducek term k f t1 ● mapReducek term k f t2
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall t1 t2 : term A,
mapReducek term k f (tm_app t1 t2) =
mapReducek term k f t1 ● mapReducek term k f t2
    test_simplification.
  Qed.

  Lemma mapReducek_term_rw4 : forall (t : term A),
      mapReducek term k f (tm_tab t) =
        mapReducek term k f t.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall t : term A,
mapReducek term k f (tm_tab t) = mapReducek term k f t
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall t : term A,
mapReducek term k f (tm_tab t) = mapReducek term k f t
    test_simplification.
  Qed.

  Lemma mapReducek_term_rw5 : forall (t: term A) (τ : typ A),
      mapReducek term k f (tm_tap t τ) =
        mapReducek term k f t ● mapReducek typ k f τ.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall (t : term A) (τ : typ A),
mapReducek term k f (tm_tap t τ) =
mapReducek term k f t ● mapReducek typ k f τ
  Proof.
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
k: K2
f: A -> M
forall (t : term A) (τ : typ A),
mapReducek term k f (tm_tap t τ) =
mapReducek term k f t ● mapReducek typ k f τ
    test_simplification.
  Qed.

End rw_mapReducek.