From Tealeaves Require Export
  Theory.DecoratedTraversableMonad
  Theory.Multisorted.DecoratedTraversableMonad
  Backends.Multisorted.LN
  Simplification.Simplification
  Simplification.MBinddt.

Export LN.Notations.

#[local] Generalizable Variables F G A B C ϕ.

(** * The index [K] *)
(******************************************************************************)
Inductive K2 : Type := ktyp | ktrm.

#[export] Instance Keq : EqDec K2 eq.
EqDec K2 eq
Proof.
EqDec K2 eq
  change (forall x y : K2, {x = y} + {x <> y}).
forall x y : K2, {x = y} + {x <> y}
  decide equality.
Defined.

#[export] Instance I2 : Index := {| K := K2 |}.

(** * System F syntax and typeclass instances *)
(******************************************************************************)
Parameter base_typ : Type.

Section syntax.

  Context
    {V : Type}.

  Inductive typ : Type :=
  | ty_c : base_typ -> typ
  | ty_v : V -> typ
  | ty_ar : typ -> typ -> typ
  | ty_univ : typ -> typ.

  Inductive term : Type :=
  | tm_var : V -> term
  | tm_abs : typ -> term -> term
  | tm_app : term -> term -> term
  | tm_tab : term -> term
  | tm_tap : term -> typ -> term.

End syntax.

(** Clear the implicit arguments to the type constructors. This keeps <<V>>
    implicit for the constructors. *)
Arguments typ V : clear implicits.
Arguments term V : clear implicits.

Definition SystemF (k : K) (v : Type) : Type :=
  match k with
  | ktyp => typ v
  | ktrm => term v
  end.

(** ** Notations *)
(******************************************************************************)
Module Notations.

  Declare Scope SystemF_scope.

  (** *** Notations for type expressions *)
  Notation "A ⟹ B" := (ty_ar A B) (at level 51, right associativity) : SystemF_scope.
  Notation "∀ τ" := (ty_univ τ) (at level 60) : SystemF_scope.

  (** *** Notations for term expressions *)
  Notation "'λ' X ⋅ body" := (tm_abs X body) (at level 45) : SystemF_scope.
  Notation "t1 @ t2" := (tm_app t1 t2) (at level 40) : SystemF_scope.
  Notation "'Λ' body" := (tm_tab body) (at level 45) : SystemF_scope.
  Notation "t1 @@ t2" := (tm_tap t1 t2) (at level 40) : SystemF_scope.

  (** *** Coercions from variables to leaves *)
  Coercion Fr : atom >-> LN.
  Coercion Bd : nat >-> LN.

  (** *** Coercions from leaves to term expressions *)
  Definition tm_var_ : LN -> term LN := @tm_var LN.
  Coercion tm_var_ : LN >-> term.

  (** *** Coercions from leaves to type expressions *)
  Definition c_base_type: base_typ -> typ LN := @ty_c LN.
  Definition c_LN_type : LN -> typ LN := @ty_v LN.
  Coercion c_base_type : base_typ >-> typ.
  Coercion c_LN_type : LN >-> typ.

End Notations.

Open Scope SystemF_scope.
Import Notations.

(** ** Example expressions *)
(******************************************************************************)
Module examples.

  Context
    (x y z : atom)
    (c1 c2 c3 : base_typ).

  (** *** Raw abstract syntax *)
  (** Abstract syntax trees without notations or coercions *)
  (******************************************************************************)

  (** *** Constants and variables *)
  Example typ_1 : typ LN := ty_v (Fr x).
  Example typ_2 : typ LN := ty_v (Fr y).
  Example typ_3 : typ LN := ty_v (Fr z).
  Example typ_4 : typ LN := ty_v (Bd 0).
  Example typ_5 : typ LN := ty_v (Bd 1).
  Example typ_6 : typ LN := ty_v (Bd 2).
  Example typ_7 : typ LN := ty_c c1.
  Example typ_8 : typ LN := ty_c c2.

  (** *** Simple types *)
  Example typ_9  : typ LN := ty_ar (ty_v (Fr x))
                                     (ty_v (Fr x)).
  Example typ_10 : typ LN := ty_ar (ty_v (Fr x))
                                     (ty_v (Fr y)).
  Example typ_11 : typ LN := ty_ar (ty_v (Fr x))
                                     (ty_v (Bd 1)).
  Example typ_12 : typ LN := ty_ar (ty_v (Bd 1))
                                     (ty_c c1).
  Example typ_13 : typ LN := ty_ar (ty_ar (ty_v (Bd 0))
                                            (ty_v (Fr x)))
                                     (ty_v (Bd 1)).
  Example typ_14 : typ LN := ty_ar (ty_c c2)
                                     (ty_ar (ty_v (Fr x))
                                            (ty_v (Bd 1))).
  Example typ_15 : typ LN := ty_ar (ty_ar (ty_v (Bd 2))
                                            (ty_c c1))
                                     (ty_ar (ty_v (Fr y))
                                            (ty_v (Fr x))).
  Example typ_16 : typ LN := ty_ar (ty_ar (ty_v (Bd 2))
                                            (ty_v (Bd 1)))
                                     (ty_ar (ty_v (Fr y))
                                            (ty_v (Fr x))).

  (** *** Universal types *)
  Example typ_17 : typ LN := ty_univ (ty_ar (ty_v (Bd 0))
                                              (ty_v (Bd 0))).
  Example typ_18 : typ LN := ty_univ (ty_ar (ty_ar (ty_v (Bd 2))
                                                     (ty_v (Bd 1)))
                                              (ty_ar (ty_v (Fr y))
                                                     (ty_v (Fr x)))).

  (** *** Printy printed syntax *)
  (******************************************************************************)
  Module pretty.

    #[local] Open Scope SystemF_scope.

    Compute (0 : typ LN).
= ty_v 0
: typ LN
    Compute (x : typ LN).
= ty_v x
: typ LN
    Compute (c1 : typ LN).
= ty_c c1
: typ LN

    (** Constants and variables *)
    Example typ_1 : typ LN := x.
    Example typ_2 : typ LN := y.
    Example typ_3 : typ LN := Fr z.
    Example typ_4 : typ LN := 0.
    Example typ_5 : typ LN := Bd 1.
    Example typ_6 : typ LN := 2.
    Example typ_7 : typ LN := c1.
    Example typ_8 : typ LN := c2.

    (** Simple types *)
    Example typ_9  : typ LN := x ⟹ x.
    Example typ_10 : typ LN := x ⟹ y.

    Goal ((x ⟹ x : typ LN) = Fr x ⟹ Fr x).
(x ⟹ x : typ LN) = x ⟹ x reflexivity. Qed.
    Goal ((x ⟹ 1 : typ LN) = Fr x ⟹ Bd 1).
(x ⟹ 1 : typ LN) = x ⟹ 1 reflexivity. Qed.

    Example typ_11 : typ LN := x ⟹ 1.
    Example typ_12 : typ LN := x ⟹ c1.
    Example typ_13 : typ LN := (x ⟹ 0) ⟹ 1.
    Example typ_14 : typ LN := c2 ⟹ (x ⟹ 1).

    Goal c2 ⟹ x ⟹ 1 = c2 ⟹ (x ⟹ 1).
c2 ⟹ x ⟹ 1 = c2 ⟹ x ⟹ 1 reflexivity. Qed.

    Example typ_15 : typ LN := (2 ⟹ c1) ⟹ (y ⟹ x).
    Example typ_16 : typ LN := (2 ⟹ 1) ⟹ (y ⟹ x).

    (** Universal types *)
    Example typ_17 : typ LN := ∀ (0 ⟹ 0).
    Goal ∀ (0 ⟹ 0) = ∀ 0 ⟹ 0.
∀ 0 ⟹ 0 = ∀ 0 ⟹ 0 reflexivity. Qed.

    Example typ_18 : typ LN := ∀ (2 ⟹ 1) ⟹ (y ⟹ x).
    Goal ∀ (2 ⟹ 1) ⟹ (y ⟹ x) = ∀ ((2 ⟹ 1) ⟹ (y ⟹ x)).
∀ (2 ⟹ 1) ⟹ y ⟹ x = ∀ (2 ⟹ 1) ⟹ y ⟹ x reflexivity. Qed.

    Example typ_19 : typ LN := (∀ 2 ⟹ 1) ⟹ (y ⟹ x).
    Example typ_20 : typ LN := (2 ⟹ 1) ⟹ ∀ y ⟹ x.

  End pretty.

  Example term_1 : term LN := tm_var (Fr x).
  Example term_2 : term LN := tm_var (Bd 0).
  Example term_3 : term LN := tm_app term_1 term_2.
  Example term_4 : term LN := tm_app term_3 term_3.

  (** Identity function on type [c1]. *)
  Example term_5 : term LN := tm_abs (ty_c c1) (tm_var (Bd 0)).
  Example term_6 : term LN := tm_app term_5 term_3.

  (** Polymorphic identity function. *)
  Example term_7 : term LN := tm_tab (tm_abs (ty_v (Bd 0))(tm_var (Bd 0))).

  (** Instantiate identity at <<c1>> *)
  Example term_8 : term LN := tm_tap term_7 c1.

  #[local] Open Scope SystemF_scope.

  Example term_9 : term LN := (Λ λ 0 ⋅ 0).

End examples.

(** ** <<binddt>> operations *)
(******************************************************************************)
Section operations.

  Context
    (F : Type -> Type)
    `{Applicative F}
    {A B : Type}.

  Fixpoint bind_type (f : forall (k : K), list K2 * A -> F (SystemF k B)) (t : typ A) : F (typ B) :=
    match t with
    | ty_c t =>
        pure (ty_c t)
    | ty_v a =>
        f ktyp (nil, a)
    | ty_ar t1 t2 =>
        pure ty_ar <⋆> bind_type f t1 <⋆> bind_type f t2
    | ty_univ body =>
        pure ty_univ <⋆> bind_type (f ◻ allK (incr [ktyp])) body
    end.

  Fixpoint bind_term (f : forall (k : K), list K2 * A -> F (SystemF k B)) (t : term A) : F (term B) :=
    match t with
    | tm_var a =>
        f ktrm (nil, a)
    | tm_abs ty body =>
        pure tm_abs
        <⋆> bind_type f ty
        <⋆> bind_term (f ◻ allK (incr [ktrm])) body
    | tm_app t1 t2 =>
        pure tm_app <⋆> bind_term f t1 <⋆> bind_term f t2
    | tm_tab body =>
        pure tm_tab <⋆> bind_term (f ◻ allK (incr [ktyp])) body
    | tm_tap t1 ty =>
        pure tm_tap <⋆> bind_term f t1 <⋆> bind_type f ty
    end.

End operations.

#[export] Instance MReturn_SystemF : MReturn SystemF :=
  fun A k => match k with
          | ktyp => ty_v
          | ktrm => tm_var
          end.

#[export] Instance MBind_type : MBind (list K2) SystemF typ := @bind_type.
#[export] Instance MBind_term : MBind (list K2) SystemF term := @bind_term.
#[export] Instance MBind_SystemF : forall k, MBind (list K2) SystemF (SystemF k) :=
  ltac:(intros [|]; typeclasses eauto).

Ltac cbn_mbinddt_post_hook ::=
  try match goal with
  | |- context[bind_type ?G ?f ?τ] =>
      change (bind_type G f τ) with (mbinddt typ G f τ)
  | |- context[bind_term ?G ?f ?t] =>
      change (bind_term G f t) with (mbinddt term G f t)
    end.

(*
Ltac simplify_mbinddt_unfold_ret_hook ::=
  unfold_ops @MReturn_SystemF.
*)

Ltac use_operational_tcs :=
  ltac_trace "use_operational_tcs";
  change (bind_type ?F ?f) with (mbinddt typ F f).

Ltac grammatical_categories_down :=
  ltac_trace "grammatical_categories_down";
  change (SystemF ktyp) with typ;
  change (MBind_SystemF ktyp) with MBind_type.

Ltac grammatical_categories_up :=
  ltac_trace "grammatical_categories_up";
  change typ with (SystemF ktyp);
  change (MBind_type) with (MBind_SystemF ktyp).

Ltac K_down :=
  ltac_trace "K_down";
  change (@K I2) with K2.

Ltac K_up :=
  ltac_trace "K_up";
  change K2 with (@K I2).

(** ** Example computations *)
(******************************************************************************)
Section example_computations.

  Open Scope SystemF_scope.

  Context
    (x y z : atom)
    (c1 c2 c3 : base_typ).

  (** ** Demo of opening operation *)
  Goal open (T := SystemF) typ ktyp (Fr x) (Bd 0) = Fr x.
x, y, z: atom
c1, c2, c3: base_typ
open typ ktyp x 0 = x reflexivity. Qed.
  Goal open typ ktyp (Fr x) (Bd 1) = Bd 0.
x, y, z: atom
c1, c2, c3: base_typ
open typ ktyp x 1 = 0 reflexivity. Qed.
  Goal open typ ktyp (Fr x) (Fr x) = Fr x.
x, y, z: atom
c1, c2, c3: base_typ
open typ ktyp x x = x reflexivity. Qed.
  Goal open typ ktyp (Fr x) (Fr y) = Fr y.
x, y, z: atom
c1, c2, c3: base_typ
open typ ktyp x y = y reflexivity. Qed.
  Goal open typ ktyp (Fr y) (Fr x) = Fr x.
x, y, z: atom
c1, c2, c3: base_typ
open typ ktyp y x = x reflexivity. Qed.
  Goal open typ ktyp (Fr y) (Fr y) = Fr y.
x, y, z: atom
c1, c2, c3: base_typ
open typ ktyp y y = y reflexivity. Qed.
  Goal open typ ktyp (Fr x) (∀ Bd 0) = (∀ (Bd 0)).
x, y, z: atom
c1, c2, c3: base_typ
open typ ktyp x (∀ 0) = ∀ 0 reflexivity. Qed.
  Goal open typ ktyp (Fr x) (∀ Bd 1) = (∀ (Fr x)).
x, y, z: atom
c1, c2, c3: base_typ
open typ ktyp x (∀ 1) = ∀ x reflexivity. Qed.
  Goal open typ ktyp (Fr x) (∀ (Bd 1 ⟹ Bd 0)) = (∀ Fr x ⟹ Bd 0).
x, y, z: atom
c1, c2, c3: base_typ
open typ ktyp x (∀ 1 ⟹ 0) = ∀ x ⟹ 0 reflexivity. Qed.
  Goal open typ ktyp (Fr x) (∀ Bd 1 ⟹ Bd 2) = (∀ Fr x ⟹ Bd 1).
x, y, z: atom
c1, c2, c3: base_typ
open typ ktyp x (∀ 1 ⟹ 2) = ∀ x ⟹ 1 reflexivity. Qed.

End example_computations.

(** * Proofs of the DTM axioms *)
(******************************************************************************)

(** ** Helper lemmas for proving DTM axioms *)
(******************************************************************************)
Section DTM_instance_lemmas.

  Context
    (W : Type)
    (S : Type -> Type)
    (T : K -> Type -> Type)
    `{! MReturn T}
    `{! MBind W T S}
    `{! forall k, MBind W T (T k)}
    {mn_op : Monoid_op W}
    {mn_unit : Monoid_unit W}.

  Lemma mbinddt_inst_law1_case1 : forall (A : Type) (t : S A) (w : W),
      (mbinddt S (fun A => A) (fun k => mret T k ∘ extract (W := (W ×))) t = t) ->
      (mbinddt S (fun A => A) (fun k => (mret T k ∘ extract (W := (W ×))) ⦿ w) t = t).
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
forall (A : Type) (t : S A) (w : W),
mbinddt S (fun A0 : Type => A0)
  (fun k : K => mret T k ∘ extract) t = t ->
mbinddt S (fun A0 : Type => A0)
  (fun k : K => (mret T k ∘ extract) ⦿ w) t = t
  Proof.
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
forall (A : Type) (t : S A) (w : W),
mbinddt S (fun A0 : Type => A0)
  (fun k : K => mret T k ∘ extract) t = t ->
mbinddt S (fun A0 : Type => A0)
  (fun k : K => (mret T k ∘ extract) ⦿ w) t = t
    introv IH.
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
A: Type
t: S A
w: W
IH: mbinddt S (fun A : Type => A)
  (fun k : K => mret T k ∘ extract) t = t
mbinddt S (fun A : Type => A)
  (fun k : K => (mret T k ∘ extract) ⦿ w) t = t rewrite <- IH at 2.
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
A: Type
t: S A
w: W
IH: mbinddt S (fun A : Type => A)
  (fun k : K => mret T k ∘ extract) t = t
mbinddt S (fun A : Type => A)
  (fun k : K => (mret T k ∘ extract) ⦿ w) t =
mbinddt S (fun A : Type => A)
  (fun k : K => mret T k ∘ extract) t
    fequal.
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
A: Type
t: S A
w: W
IH: mbinddt S (fun A : Type => A)
  (fun k : K => mret T k ∘ extract) t = t
(fun k : K => (mret T k ∘ extract) ⦿ w) =
(fun k : K => mret T k ∘ extract) ext k [w' a].
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
A: Type
t: S A
w: W
IH: mbinddt S (fun A : Type => A)
  (fun k : K => mret T k ∘ extract) t = t
k: K
w': W
a: A
((mret T k ∘ extract) ⦿ w) (w', a) =
(mret T k ∘ extract) (w', a) easy.
  Qed.

  Lemma mbinddt_inst_law1_case12 : forall (A : Type) (w : W),
      mbinddt S (fun A => A) (fun k => mret T k ∘ extract (W := (W ×))) (A := A) =
        mbinddt S (fun A => A) ((fun k => mret T k ∘ extract (W := (W ×))) ◻ allK (incr w)).
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
forall (A : Type) (w : W),
mbinddt S (fun A0 : Type => A0)
  (fun k : K => mret T k ∘ extract) =
mbinddt S (fun A0 : Type => A0)
  ((fun k : K => mret T k ∘ extract) ◻ allK (incr w))
  Proof.
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
forall (A : Type) (w : W),
mbinddt S (fun A0 : Type => A0)
  (fun k : K => mret T k ∘ extract) =
mbinddt S (fun A0 : Type => A0)
  ((fun k : K => mret T k ∘ extract) ◻ allK (incr w))
    introv.
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
A: Type
w: W
mbinddt S (fun A : Type => A)
  (fun k : K => mret T k ∘ extract) =
mbinddt S (fun A : Type => A)
  ((fun k : K => mret T k ∘ extract) ◻ allK (incr w)) fequal.
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
A: Type
w: W
(fun k : K => mret T k ∘ extract) =
(fun k : K => mret T k ∘ extract) ◻ allK (incr w) now ext k [w' a].
  Qed.

  Context
    `{Applicative G}
    `{Applicative F}
    `{! Monoid W}
    {A B C : Type}
    (g : forall k, W * B -> G (T k C))
    (f : forall k, W * A -> F (T k B)).

  (* for Var case *)
  Lemma mbinddt_inst_law2_case2 : forall (a : A) (k : K),
    map (F := F) (mbinddt (T k) G g) (f k (Ƶ, a)) =
    map (F := F) (mbinddt (T k) G (g ◻ allK (incr Ƶ))) (f k (Ƶ, a)).
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
F: Type -> Type
Map_G0: Map F
Pure_G0: Pure F
Mult_G0: Mult F
H1: Applicative F
Monoid0: Monoid W
A, B, C: Type
g: forall k : K, W * B -> G (T k C)
f: forall k : K, W * A -> F (T k B)
forall (a : A) (k : K),
map (mbinddt (T k) G g) (f k (Ƶ, a)) =
map (mbinddt (T k) G (g ◻ allK (incr Ƶ))) (f k (Ƶ, a))
  Proof.
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
F: Type -> Type
Map_G0: Map F
Pure_G0: Pure F
Mult_G0: Mult F
H1: Applicative F
Monoid0: Monoid W
A, B, C: Type
g: forall k : K, W * B -> G (T k C)
f: forall k : K, W * A -> F (T k B)
forall (a : A) (k : K),
map (mbinddt (T k) G g) (f k (Ƶ, a)) =
map (mbinddt (T k) G (g ◻ allK (incr Ƶ))) (f k (Ƶ, a))
    intros.
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
F: Type -> Type
Map_G0: Map F
Pure_G0: Pure F
Mult_G0: Mult F
H1: Applicative F
Monoid0: Monoid W
A, B, C: Type
g: forall k : K, W * B -> G (T k C)
f: forall k : K, W * A -> F (T k B)
a: A
k: K
map (mbinddt (T k) G g) (f k (Ƶ, a)) =
map (mbinddt (T k) G (g ◻ allK (incr Ƶ))) (f k (Ƶ, a))
    repeat fequal.
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
F: Type -> Type
Map_G0: Map F
Pure_G0: Pure F
Mult_G0: Mult F
H1: Applicative F
Monoid0: Monoid W
A, B, C: Type
g: forall k : K, W * B -> G (T k C)
f: forall k : K, W * A -> F (T k B)
a: A
k: K
g = g ◻ allK (incr Ƶ)
    ext k' [w b].
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
F: Type -> Type
Map_G0: Map F
Pure_G0: Pure F
Mult_G0: Mult F
H1: Applicative F
Monoid0: Monoid W
A, B, C: Type
g: forall k : K, W * B -> G (T k C)
f: forall k : K, W * A -> F (T k B)
a: A
k, k': K
w: W
b: B
g k' (w, b) = (g ◻ allK (incr Ƶ)) k' (w, b)
    rewrite vec_compose_allK2.
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
F: Type -> Type
Map_G0: Map F
Pure_G0: Pure F
Mult_G0: Mult F
H1: Applicative F
Monoid0: Monoid W
A, B, C: Type
g: forall k : K, W * B -> G (T k C)
f: forall k : K, W * A -> F (T k B)
a: A
k, k': K
w: W
b: B
g k' (w, b) = (g k' ∘ incr Ƶ) (w, b)
    unfold compose.
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
F: Type -> Type
Map_G0: Map F
Pure_G0: Pure F
Mult_G0: Mult F
H1: Applicative F
Monoid0: Monoid W
A, B, C: Type
g: forall k : K, W * B -> G (T k C)
f: forall k : K, W * A -> F (T k B)
a: A
k, k': K
w: W
b: B
g k' (w, b) = g k' (incr Ƶ (w, b)) cbn.
W: Type
S: Type -> Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T S
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
F: Type -> Type
Map_G0: Map F
Pure_G0: Pure F
Mult_G0: Mult F
H1: Applicative F
Monoid0: Monoid W
A, B, C: Type
g: forall k : K, W * B -> G (T k C)
f: forall k : K, W * A -> F (T k B)
a: A
k, k': K
w: W
b: B
g k' (w, b) = g k' (Ƶ ● w, b)
    now simpl_monoid.
  Qed.

End DTM_instance_lemmas.

(** ** <<mbinddt_mret>> *)
(******************************************************************************)
Lemma mbinddt_mret_typ : forall (A: Type),
    mbinddt typ (fun A => A) (mret SystemF ◻ allK extract) = @id (typ A).
forall A : Type,
mbinddt typ (fun A0 : Type => A0)
  (mret SystemF ◻ allK extract) = id
Proof.
forall A : Type,
mbinddt typ (fun A0 : Type => A0)
  (mret SystemF ◻ allK extract) = id
  intros.
A: Type
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) = id ext t.
A: Type
t: typ A
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t = id t unfold id.
A: Type
t: typ A
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t = t induction t.
A: Type
b: base_typ
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) (ty_c b) = ty_c b
A: Type
v: A
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) (ty_v v) = ty_v v
A: Type
t1, t2: typ A
IHt1: mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
IHt2: mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) (t1 ⟹ t2) = t1 ⟹ t2
A: Type
t: typ A
IHt: mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t = t
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) 
  (∀ t) = ∀ t
  -
A: Type
b: base_typ
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) (ty_c b) = ty_c b simplify_mbinddt.
A: Type
b: base_typ
pure (ty_c b) = ty_c b reflexivity.
  -
A: Type
v: A
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) (ty_v v) = ty_v v simplify_mbinddt.
A: Type
v: A
ty_v v = ty_v v reflexivity.
  -
A: Type
t1, t2: typ A
IHt1: mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
IHt2: mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) (t1 ⟹ t2) = t1 ⟹ t2 simplify_mbinddt.
A: Type
t1, t2: typ A
IHt1: mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
IHt2: mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
pure ty_ar
  (mbinddt typ (fun A : Type => A)
     (mret SystemF ◻ allK extract) t1)
  (mbinddt typ (fun A : Type => A)
     (mret SystemF ◻ allK extract) t2) = t1 ⟹ t2
    fequal.
A: Type
t1, t2: typ A
IHt1: mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
IHt2: mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
A: Type
t1, t2: typ A
IHt1: mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
IHt2: mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
    apply IHt1.
A: Type
t1, t2: typ A
IHt1: mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
IHt2: mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
    apply IHt2.
  -
A: Type
t: typ A
IHt: mbinddt typ (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) (∀ t) = ∀ t cbn.
A: Type
t: typ A
IHt: mbinddt typ (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
pure ty_univ
  (mbinddt typ (fun A : Type => A)
     ((mret SystemF ◻ allK extract)
      ◻ allK (incr [ktyp])) t) = ∀ t fequal.
A: Type
t: typ A
IHt: mbinddt typ (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt typ (fun A : Type => A)
  ((mret SystemF ◻ allK extract) ◻ allK (incr [ktyp]))
  t = t
    rewrite vec_compose_assoc.
A: Type
t: typ A
IHt: mbinddt typ (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ (allK extract ◻ allK (incr [ktyp])))
  t = t
    K_up.
A: Type
t: typ A
IHt: mbinddt typ (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ (allK extract ◻ allK (incr [ktyp])))
  t = t
    rewrite vec_compose_allK.
A: Type
t: typ A
IHt: mbinddt typ (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK (extract ∘ incr [ktyp])) t = t
    rewrite extract_incr.
A: Type
t: typ A
IHt: mbinddt typ (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t = t
    assumption.
Qed.

Lemma mbinddt_mret_term : forall (A : Type),
    mbinddt term (fun A => A) (mret SystemF ◻ allK (extract (W := (list K2 ×)))) = @id (term A).
forall A : Type,
mbinddt term (fun A0 : Type => A0)
  (mret SystemF ◻ allK extract) = id
Proof.
forall A : Type,
mbinddt term (fun A0 : Type => A0)
  (mret SystemF ◻ allK extract) = id
  intros.
A: Type
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) = id ext t.
A: Type
t: term A
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t = id t unfold id.
A: Type
t: term A
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t = t induction t.
A: Type
v: A
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) (tm_var v) = tm_var v
A: Type
t: typ A
t0: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t0 = t0
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) (λ t ⋅ t0) = λ t ⋅ t0
A: Type
t1, t2: term A
IHt1: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
IHt2: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) (t1 @ t2) = t1 @ t2
A: Type
t: term A
IHt: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t = t
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) 
  (Λ t) = Λ t
A: Type
t: term A
t0: typ A
IHt: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t = t
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) 
  (t @@ t0) = t @@ t0
  -
A: Type
v: A
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) (tm_var v) = tm_var v simplify_mbinddt.
A: Type
v: A
tm_var v = tm_var v reflexivity.
  -
A: Type
t: typ A
t0: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t0 = t0
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) (λ t ⋅ t0) = λ t ⋅ t0 cbn_mbinddt.
A: Type
t: typ A
t0: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t0 = t0
pure tm_abs
  (mbinddt typ (fun A : Type => A)
     (mret SystemF ◻ allK extract) t)
  (mbinddt term (fun A : Type => A)
     ((mret SystemF ◻ allK extract)
      ◻ allK (incr [ktrm])) t0) = λ t ⋅ t0
    fequal
    + use_operational_tcs.
A: Type
t: typ A
t0: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t0 = t0
mbinddt typ (fun A : Type => A)
  (mret SystemF ◻ allK extract) t = t
A: Type
t: typ A
t0: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t0 = t0
mbinddt term (fun A : Type => A)
  ((mret SystemF ◻ allK extract) ◻ allK (incr [ktrm]))
  t0 = t0
      now rewrite mbinddt_mret_typ.
A: Type
t: typ A
t0: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t0 = t0
mbinddt term (fun A : Type => A)
  ((mret SystemF ◻ allK extract) ◻ allK (incr [ktrm]))
  t0 = t0
    +
A: Type
t: typ A
t0: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t0 = t0
mbinddt term (fun A : Type => A)
  ((mret SystemF ◻ allK extract) ◻ allK (incr [ktrm]))
  t0 = t0 rewrite vec_compose_assoc.
A: Type
t: typ A
t0: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t0 = t0
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ (allK extract ◻ allK (incr [ktrm])))
  t0 = t0
      K_up.
A: Type
t: typ A
t0: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t0 = t0
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ (allK extract ◻ allK (incr [ktrm])))
  t0 = t0
      rewrite vec_compose_allK.
A: Type
t: typ A
t0: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t0 = t0
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK (extract ∘ incr [ktrm])) t0 =
t0
      rewrite extract_incr.
A: Type
t: typ A
t0: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t0 = t0
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t0 = t0
      assumption.
  -
A: Type
t1, t2: term A
IHt1: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
IHt2: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) (t1 @ t2) = t1 @ t2 cbn.
A: Type
t1, t2: term A
IHt1: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
IHt2: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
pure tm_app
  (mbinddt term (fun A : Type => A)
     (mret SystemF ◻ allK extract) t1)
  (mbinddt term (fun A : Type => A)
     (mret SystemF ◻ allK extract) t2) = t1 @ t2 fequal.
A: Type
t1, t2: term A
IHt1: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
IHt2: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
A: Type
t1, t2: term A
IHt1: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
IHt2: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
    +
A: Type
t1, t2: term A
IHt1: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
IHt2: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1 apply IHt1.
    +
A: Type
t1, t2: term A
IHt1: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t1 = t1
IHt2: mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t2 = t2 apply IHt2.
  -
A: Type
t: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) (Λ t) = Λ t cbn.
A: Type
t: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
pure tm_tab
  (mbinddt term (fun A : Type => A)
     ((mret SystemF ◻ allK extract)
      ◻ allK (incr [ktyp])) t) = Λ t fequal.
A: Type
t: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt term (fun A : Type => A)
  ((mret SystemF ◻ allK extract) ◻ allK (incr [ktyp]))
  t = t
    rewrite vec_compose_assoc.
A: Type
t: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ (allK extract ◻ allK (incr [ktyp])))
  t = t
    K_up.
A: Type
t: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ (allK extract ◻ allK (incr [ktyp])))
  t = t
    rewrite vec_compose_allK.
A: Type
t: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK (extract ∘ incr [ktyp])) t = t
    rewrite extract_incr.
A: Type
t: term A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t = t
    assumption.
  -
A: Type
t: term A
t0: typ A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) (t @@ t0) = t @@ t0 cbn.
A: Type
t: term A
t0: typ A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
pure tm_tap
  (mbinddt term (fun A : Type => A)
     (mret SystemF ◻ allK extract) t)
  (bind_type (fun A : Type => A)
     (mret SystemF ◻ allK extract) t0) = t @@ t0 fequal.
A: Type
t: term A
t0: typ A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t = t
A: Type
t: term A
t0: typ A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
bind_type (fun A : Type => A)
  (mret SystemF ◻ allK extract) t0 = t0
    +
A: Type
t: term A
t0: typ A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
mbinddt term (fun A : Type => A)
  (mret SystemF ◻ allK extract) t = t apply IHt.
    +
A: Type
t: term A
t0: typ A
IHt: mbinddt term (fun A : Type => A) (mret SystemF ◻ allK extract) t = t
bind_type (fun A : Type => A)
  (mret SystemF ◻ allK extract) t0 = t0 now rewrite mbinddt_mret_typ.
Qed.

(** ** <<mbinddt_mbinddt>> *)
(******************************************************************************)
Lemma mbinddt_mbinddt_typ :
  forall (F : Type -> Type)
    (G : Type -> Type)
    `{Applicative F}
    `{Applicative G}
    `(g : forall k, list K2 * B -> G (SystemF k C))
    `(f : forall k, list K2 * A -> F (SystemF k B)),
    map (F := F) (mbinddt typ G g) ∘ mbinddt typ F f =
    mbinddt typ (F ∘ G) (g ⋆dtm f).
forall (F G : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (Map_G0 : Map G) (Pure_G0 : Pure G)
  (Mult_G0 : Mult G),
Applicative G ->
forall (B C : Type)
  (g : forall k : K, list K2 * B -> G (SystemF k C))
  (A : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) ∘ mbinddt typ F f =
mbinddt typ (F ∘ G) (g ⋆dtm f)
Proof.
forall (F G : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (Map_G0 : Map G) (Pure_G0 : Pure G)
  (Mult_G0 : Mult G),
Applicative G ->
forall (B C : Type)
  (g : forall k : K, list K2 * B -> G (SystemF k C))
  (A : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) ∘ mbinddt typ F f =
mbinddt typ (F ∘ G) (g ⋆dtm f)
  intros.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C: Type
g: forall k : K, list K2 * B -> G (SystemF k C)
A: Type
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g) ∘ mbinddt typ F f =
mbinddt typ (F ∘ G) (g ⋆dtm f) ext t.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C: Type
g: forall k : K, list K2 * B -> G (SystemF k C)
A: Type
f: forall k : K, list K2 * A -> F (SystemF k B)
t: typ A
(map (mbinddt typ G g) ∘ mbinddt typ F f) t =
mbinddt typ (F ∘ G) (g ⋆dtm f) t generalize dependent f.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C: Type
g: forall k : K, list K2 * B -> G (SystemF k C)
A: Type
t: typ A
forall
  f : forall k : K, list K2 * A -> F (SystemF k B),
(map (mbinddt typ G g) ∘ mbinddt typ F f) t =
mbinddt typ (F ∘ G) (g ⋆dtm f) t generalize dependent g.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
forall
  (g : forall k : K, list K2 * B -> G (SystemF k C))
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
(map (mbinddt typ G g) ∘ mbinddt typ F f) t =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
  unfold compose at 1.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
forall
  (g : forall k : K, list K2 * B -> G (SystemF k C))
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t induction t; intros g f.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
b: base_typ
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g) (mbinddt typ F f (ty_c b)) =
mbinddt typ (F ∘ G) (g ⋆dtm f) (ty_c b)
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g) (mbinddt typ F f (ty_v v)) =
mbinddt typ (F ∘ G) (g ⋆dtm f) (ty_v v)
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g) (mbinddt typ F f (t1 ⟹ t2)) =
mbinddt typ (F ∘ G) (g ⋆dtm f) (t1 ⟹ t2)
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g) (mbinddt typ F f (∀ t)) =
mbinddt typ (F ∘ G) (g ⋆dtm f) (∀ t)
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
b: base_typ
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g) (mbinddt typ F f (ty_c b)) =
mbinddt typ (F ∘ G) (g ⋆dtm f) (ty_c b) cbn.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
b: base_typ
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g) (pure (ty_c b)) = pure (ty_c b)
    rewrite (app_pure_natural).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
b: base_typ
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
pure (mbinddt typ G g (ty_c b)) = pure (ty_c b)
    reflexivity.
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g) (mbinddt typ F f (ty_v v)) =
mbinddt typ (F ∘ G) (g ⋆dtm f) (ty_v v) cbn.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g) (f ktyp ([], v)) =
map
  (MBind_type G Map_G0 Pure_G0 Mult_G0 B C
     (g ◻ allK (incr []))) (f ktyp ([], v))
    change (MBind_type ?G ?Map ?Pure ?Mult ?A ?B) with
      (mbinddt typ G (A := A) (B := B)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g) (f ktyp ([], v)) =
map (mbinddt typ G (g ◻ allK (incr [])))
  (f ktyp ([], v))
    change [] with (Ƶ : list K2).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g) (f ktyp (Ƶ : list K2, v)) =
map (mbinddt typ G (g ◻ allK (incr (Ƶ : list K2))))
  (f ktyp (Ƶ : list K2, v))
    change typ with (SystemF ktyp).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt (SystemF ktyp) G g)
  (f ktyp (Ƶ : list K2, v)) =
map
  (mbinddt (SystemF ktyp) G
     (g ◻ allK (incr (Ƶ : list K2))))
  (f ktyp (Ƶ : list K2, v))
    unfold vec_compose.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt (SystemF ktyp) G g) (f ktyp (Ƶ, v)) =
map
  (mbinddt (SystemF ktyp) G
     (fun k : K => g k ∘ allK (incr Ƶ) k))
  (f ktyp (Ƶ, v))
    Set Keyed Unification.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt (SystemF ktyp) G g) (f ktyp (Ƶ, v)) =
map
  (mbinddt (SystemF ktyp) G
     (fun k : K => g k ∘ allK (incr Ƶ) k))
  (f ktyp (Ƶ, v))
    rewrite <- (mbinddt_inst_law2_case2 (list K2)
                 SystemF (H := MBind_SystemF) _ _ _ ktyp).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt (SystemF ktyp) G g) (f ktyp (Ƶ, v)) =
map (mbinddt (SystemF ktyp) G g) (f ktyp (Ƶ, v))
    Unset Keyed Unification.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt (SystemF ktyp) G g) (f ktyp (Ƶ, v)) =
map (mbinddt (SystemF ktyp) G g) (f ktyp (Ƶ, v))
    reflexivity.
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g) (mbinddt typ F f (t1 ⟹ t2)) =
mbinddt typ (F ∘ G) (g ⋆dtm f) (t1 ⟹ t2) cbn.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g)
  (pure ty_ar <⋆> mbinddt typ F f t1 <⋆>
   mbinddt typ F f t2) =
pure ty_ar <⋆> mbinddt typ (F ∘ G) (g ⋆dtm f) t1 <⋆>
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
    rewrite <- IHt1.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g)
  (pure ty_ar <⋆> mbinddt typ F f t1 <⋆>
   mbinddt typ F f t2) =
pure ty_ar <⋆>
map (mbinddt typ G g) (mbinddt typ F f t1) <⋆>
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
    rewrite <- IHt2.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g)
  (pure ty_ar <⋆> mbinddt typ F f t1 <⋆>
   mbinddt typ F f t2) =
pure ty_ar <⋆>
map (mbinddt typ G g) (mbinddt typ F f t1) <⋆>
map (mbinddt typ G g) (mbinddt typ F f t2)
    do 2 rewrite (ap_compose2 G F).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g)
  (pure ty_ar <⋆> mbinddt typ F f t1 <⋆>
   mbinddt typ F f t2) =
map (ap G)
  (map (ap G) (pure ty_ar) <⋆>
   map (mbinddt typ G g) (mbinddt typ F f t1)) <⋆>
map (mbinddt typ G g) (mbinddt typ F f t2)
    rewrite <- (ap_map (G := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g)
  (pure ty_ar <⋆> mbinddt typ F f t1 <⋆>
   mbinddt typ F f t2) =
map (precompose (mbinddt typ G g))
  (map (ap G)
     (map (ap G) (pure ty_ar) <⋆>
      map (mbinddt typ G g) (mbinddt typ F f t1))) <⋆>
mbinddt typ F f t2
    rewrite <- (ap_map (G := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g)
  (pure ty_ar <⋆> mbinddt typ F f t1 <⋆>
   mbinddt typ F f t2) =
map (precompose (mbinddt typ G g))
  (map (ap G)
     (map (precompose (mbinddt typ G g))
        (map (ap G) (pure ty_ar)) <⋆>
      mbinddt typ F f t1)) <⋆> mbinddt typ F f t2
    do 2 rewrite map_ap.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (compose (compose (mbinddt typ G g))) (pure ty_ar) <⋆>
mbinddt typ F f t1 <⋆> mbinddt typ F f t2 =
map (precompose (mbinddt typ G g))
  (map (ap G)
     (map (precompose (mbinddt typ G g))
        (map (ap G) (pure ty_ar)) <⋆>
      mbinddt typ F f t1)) <⋆> mbinddt typ F f t2
    do 2 rewrite map_ap.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (compose (compose (mbinddt typ G g))) (pure ty_ar) <⋆>
mbinddt typ F f t1 <⋆> mbinddt typ F f t2 =
map (compose (precompose (mbinddt typ G g)))
  (map (compose (ap G))
     (map (precompose (mbinddt typ G g))
        (map (ap G) (pure ty_ar)))) <⋆>
mbinddt typ F f t1 <⋆> mbinddt typ F f t2
    assert (Functor F) by apply app_functor.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt typ G g))) (pure ty_ar) <⋆>
mbinddt typ F f t1 <⋆> mbinddt typ F f t2 =
map (compose (precompose (mbinddt typ G g)))
  (map (compose (ap G))
     (map (precompose (mbinddt typ G g))
        (map (ap G) (pure ty_ar)))) <⋆>
mbinddt typ F f t1 <⋆> mbinddt typ F f t2
    do 3 (compose near (pure (F := (F ∘ G)) (ty_ar (V := C)));
          rewrite (fun_map_map (F := F))).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt typ G g))) (pure ty_ar) <⋆>
mbinddt typ F f t1 <⋆> mbinddt typ F f t2 =
map
  (compose (precompose (mbinddt typ G g))
   ∘ (compose (ap G)
      ∘ (precompose (mbinddt typ G g) ∘ ap G)))
  (pure ty_ar) <⋆> mbinddt typ F f t1 <⋆>
mbinddt typ F f t2
    unfold_ops @Pure_compose.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt typ G g))) (pure ty_ar) <⋆>
mbinddt typ F f t1 <⋆> mbinddt typ F f t2 =
map
  (compose (precompose (mbinddt typ G g))
   ∘ (compose (ap G)
      ∘ (precompose (mbinddt typ G g) ∘ ap G)))
  (pure (pure ty_ar)) <⋆> mbinddt typ F f t1 <⋆>
mbinddt typ F f t2
    rewrite (app_pure_natural).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
pure (compose (mbinddt typ G g) ∘ ty_ar) <⋆>
mbinddt typ F f t1 <⋆> mbinddt typ F f t2 =
map
  (compose (precompose (mbinddt typ G g))
   ∘ (compose (ap G)
      ∘ (precompose (mbinddt typ G g) ∘ ap G)))
  (pure (pure ty_ar)) <⋆> mbinddt typ F f t1 <⋆>
mbinddt typ F f t2
    rewrite (app_pure_natural).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: typ A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t1) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t2) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
pure (compose (mbinddt typ G g) ∘ ty_ar) <⋆>
mbinddt typ F f t1 <⋆> mbinddt typ F f t2 =
pure
  ((compose (precompose (mbinddt typ G g))
    ∘ (compose (ap G)
       ∘ (precompose (mbinddt typ G g) ∘ ap G)))
     (pure ty_ar)) <⋆> mbinddt typ F f t1 <⋆>
mbinddt typ F f t2
    reflexivity.
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g) (mbinddt typ F f (∀ t)) =
mbinddt typ (F ∘ G) (g ⋆dtm f) (∀ t) cbn.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g)
  (pure ty_univ <⋆>
   mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
pure ty_univ <⋆>
mbinddt typ (F ∘ G) (g ⋆dtm f ◻ allK (incr [ktyp])) t
    setoid_rewrite compose_dtm_incr_alt.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g)
  (pure ty_univ <⋆>
   mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
pure ty_univ <⋆>
mbinddt typ (F ∘ G)
  ((g ◻ allK (incr [ktyp]))
   ⋆dtm (f ◻ allK (incr [ktyp]))) t
    rewrite <- IHt.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g)
  (pure ty_univ <⋆>
   mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
pure ty_univ <⋆>
map (mbinddt typ G (g ◻ allK (incr [ktyp])))
  (mbinddt typ F (f ◻ allK (incr [ktyp])) t)
    rewrite (ap_compose2 G F).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g)
  (pure ty_univ <⋆>
   mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
map (ap G) (pure ty_univ) <⋆>
map (mbinddt typ G (g ◻ allK (incr [ktyp])))
  (mbinddt typ F (f ◻ allK (incr [ktyp])) t)
    rewrite <- (ap_map (G := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g)
  (pure ty_univ <⋆>
   mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
map
  (precompose (mbinddt typ G (g ◻ allK (incr [ktyp]))))
  (map (ap G) (pure ty_univ)) <⋆>
mbinddt typ F (f ◻ allK (incr [ktyp])) t
    compose near (pure (F := F ∘ G) (ty_univ (V := C))).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt typ G g)
  (pure ty_univ <⋆>
   mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
(map
   (precompose
      (mbinddt typ G (g ◻ allK (incr [ktyp]))))
 ∘ map (ap G)) (pure ty_univ) <⋆>
mbinddt typ F (f ◻ allK (incr [ktyp])) t
    assert (Functor F) by apply app_functor.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt typ G g)
  (pure ty_univ <⋆>
   mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
(map
   (precompose
      (mbinddt typ G (g ◻ allK (incr [ktyp]))))
 ∘ map (ap G)) (pure ty_univ) <⋆>
mbinddt typ F (f ◻ allK (incr [ktyp])) t
    rewrite (fun_map_map (F := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt typ G g)
  (pure ty_univ <⋆>
   mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
map
  (precompose (mbinddt typ G (g ◻ allK (incr [ktyp])))
   ∘ ap G) (pure ty_univ) <⋆>
mbinddt typ F (f ◻ allK (incr [ktyp])) t
    unfold_ops @Pure_compose.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt typ G g)
  (pure ty_univ <⋆>
   mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
map
  (precompose (mbinddt typ G (g ◻ allK (incr [ktyp])))
   ∘ ap G) (pure (pure ty_univ)) <⋆>
mbinddt typ F (f ◻ allK (incr [ktyp])) t
    rewrite (app_pure_natural).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt typ G g)
  (pure ty_univ <⋆>
   mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
pure
  ((precompose
      (mbinddt typ G (g ◻ allK (incr [ktyp]))) ∘ ap G)
     (pure ty_univ)) <⋆>
mbinddt typ F (f ◻ allK (incr [ktyp])) t
    rewrite map_ap.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (mbinddt typ G g)) (pure ty_univ) <⋆>
mbinddt typ F (f ◻ allK (incr [ktyp])) t =
pure
  ((precompose
      (mbinddt typ G (g ◻ allK (incr [ktyp]))) ∘ ap G)
     (pure ty_univ)) <⋆>
mbinddt typ F (f ◻ allK (incr [ktyp])) t
    rewrite (app_pure_natural).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt typ G g) (mbinddt typ F f t) =
mbinddt typ (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
pure (mbinddt typ G g ∘ ty_univ) <⋆>
mbinddt typ F (f ◻ allK (incr [ktyp])) t =
pure
  ((precompose
      (mbinddt typ G (g ◻ allK (incr [ktyp]))) ∘ ap G)
     (pure ty_univ)) <⋆>
mbinddt typ F (f ◻ allK (incr [ktyp])) t
    reflexivity.
Qed.

Lemma mbinddt_mbinddt_term :
  forall (F : Type -> Type)
    (G : Type -> Type)
    `{Applicative F}
    `{Applicative G}
    `(g : forall k, list K2 * B -> G (SystemF k C))
    `(f : forall k, list K2 * A -> F (SystemF k B)),
    map (F := F) (mbinddt term G g) ∘ mbinddt term F f =
    mbinddt term (F ∘ G) (g ⋆dtm f).
forall (F G : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (Map_G0 : Map G) (Pure_G0 : Pure G)
  (Mult_G0 : Mult G),
Applicative G ->
forall (B C : Type)
  (g : forall k : K, list K2 * B -> G (SystemF k C))
  (A : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) ∘ mbinddt term F f =
mbinddt term (F ∘ G) (g ⋆dtm f)
Proof.
forall (F G : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (Map_G0 : Map G) (Pure_G0 : Pure G)
  (Mult_G0 : Mult G),
Applicative G ->
forall (B C : Type)
  (g : forall k : K, list K2 * B -> G (SystemF k C))
  (A : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) ∘ mbinddt term F f =
mbinddt term (F ∘ G) (g ⋆dtm f)
  intros.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C: Type
g: forall k : K, list K2 * B -> G (SystemF k C)
A: Type
f: forall k : K, list K2 * A -> F (SystemF k B)
map (mbinddt term G g) ∘ mbinddt term F f =
mbinddt term (F ∘ G) (g ⋆dtm f) ext t.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C: Type
g: forall k : K, list K2 * B -> G (SystemF k C)
A: Type
f: forall k : K, list K2 * A -> F (SystemF k B)
t: term A
(map (mbinddt term G g) ∘ mbinddt term F f) t =
mbinddt term (F ∘ G) (g ⋆dtm f) t generalize dependent f.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C: Type
g: forall k : K, list K2 * B -> G (SystemF k C)
A: Type
t: term A
forall
  f : forall k : K, list K2 * A -> F (SystemF k B),
(map (mbinddt term G g) ∘ mbinddt term F f) t =
mbinddt term (F ∘ G) (g ⋆dtm f) t generalize dependent g.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
forall
  (g : forall k : K, list K2 * B -> G (SystemF k C))
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
(map (mbinddt term G g) ∘ mbinddt term F f) t =
mbinddt term (F ∘ G) (g ⋆dtm f) t
  unfold compose at 1.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
forall
  (g : forall k : K, list K2 * B -> G (SystemF k C))
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t induction t; intros g f;
    assert (Functor F) by apply app_functor.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g) (mbinddt term F f (tm_var v)) =
mbinddt term (F ∘ G) (g ⋆dtm f) (tm_var v)
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g) (mbinddt term F f (λ t ⋅ t0)) =
mbinddt term (F ∘ G) (g ⋆dtm f) (λ t ⋅ t0)
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g) (mbinddt term F f (t1 @ t2)) =
mbinddt term (F ∘ G) (g ⋆dtm f) (t1 @ t2)
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g) (mbinddt term F f (Λ t)) =
mbinddt term (F ∘ G) (g ⋆dtm f) (Λ t)
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g) (mbinddt term F f (t @@ t0)) =
mbinddt term (F ∘ G) (g ⋆dtm f) (t @@ t0)
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g) (mbinddt term F f (tm_var v)) =
mbinddt term (F ∘ G) (g ⋆dtm f) (tm_var v) cbn.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g) (f ktrm ([], v)) =
map
  (MBind_term G Map_G0 Pure_G0 Mult_G0 B C
     (g ◻ allK (incr []))) (f ktrm ([], v))
    change (MBind_term ?G ?map ?pure ?mult ?A ?B) with
      (mbinddt term G (A := A) (B := B)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g) (f ktrm ([], v)) =
map (mbinddt term G (g ◻ allK (incr [])))
  (f ktrm ([], v))
    fequal.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
mbinddt term G g = mbinddt term G (g ◻ allK (incr [])) fequal.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
v: A
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
g = g ◻ allK (incr []) now ext k [w a].
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g) (mbinddt term F f (λ t ⋅ t0)) =
mbinddt term (F ∘ G) (g ⋆dtm f) (λ t ⋅ t0) cbn.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_abs <⋆> bind_type F f t <⋆>
   mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
pure tm_abs <⋆> bind_type (F ∘ G) (g ⋆dtm f) t <⋆>
mbinddt term (F ∘ G) (g ⋆dtm f ◻ allK (incr [ktrm]))
  t0
    change (bind_type ?F ?f) with (mbinddt typ F f).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_abs <⋆> mbinddt typ F f t <⋆>
   mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
pure tm_abs <⋆> mbinddt typ (F ∘ G) (g ⋆dtm f) t <⋆>
mbinddt term (F ∘ G) (g ⋆dtm f ◻ allK (incr [ktrm]))
  t0
    setoid_rewrite compose_dtm_incr_alt.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_abs <⋆> mbinddt typ F f t <⋆>
   mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
pure tm_abs <⋆> mbinddt typ (F ∘ G) (g ⋆dtm f) t <⋆>
mbinddt term (F ∘ G)
  ((g ◻ allK (incr [ktrm]))
   ⋆dtm (f ◻ allK (incr [ktrm]))) t0
    rewrite <- IHt.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_abs <⋆> mbinddt typ F f t <⋆>
   mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
pure tm_abs <⋆> mbinddt typ (F ∘ G) (g ⋆dtm f) t <⋆>
map (mbinddt term G (g ◻ allK (incr [ktrm])))
  (mbinddt term F (f ◻ allK (incr [ktrm])) t0)
    rewrite <- (mbinddt_mbinddt_typ F G).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_abs <⋆> mbinddt typ F f t <⋆>
   mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
pure tm_abs <⋆>
(map (mbinddt typ G g) ∘ mbinddt typ F f) t <⋆>
map (mbinddt term G (g ◻ allK (incr [ktrm])))
  (mbinddt term F (f ◻ allK (incr [ktrm])) t0)
    unfold compose at 2.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_abs <⋆> mbinddt typ F f t <⋆>
   mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
pure tm_abs <⋆>
(map (mbinddt typ G g) ∘ mbinddt typ F f) t <⋆>
map (mbinddt term G (g ◻ allK (incr [ktrm])))
  (mbinddt term F (f ◻ allK (incr [ktrm])) t0)
    do 2 rewrite (ap_compose2 G F).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_abs <⋆> mbinddt typ F f t <⋆>
   mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
map (ap G)
  (map (ap G) (pure tm_abs) <⋆>
   (map (mbinddt typ G g) ∘ mbinddt typ F f) t) <⋆>
map (mbinddt term G (g ◻ allK (incr [ktrm])))
  (mbinddt term F (f ◻ allK (incr [ktrm])) t0)
    unfold compose.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_abs <⋆> mbinddt typ F f t <⋆>
   mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
map (ap G)
  (map (ap G) (pure tm_abs) <⋆>
   map (mbinddt typ G g) (mbinddt typ F f t)) <⋆>
map (mbinddt term G (g ◻ allK (incr [ktrm])))
  (mbinddt term F (f ◻ allK (incr [ktrm])) t0)
    do 2 rewrite <- (ap_map (G := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_abs <⋆> mbinddt typ F f t <⋆>
   mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
map
  (precompose
     (mbinddt term G (g ◻ allK (incr [ktrm]))))
  (map (ap G)
     (map (precompose (mbinddt typ G g))
        (map (ap G) (pure tm_abs)) <⋆>
      mbinddt typ F f t)) <⋆>
mbinddt term F (f ◻ allK (incr [ktrm])) t0
    unfold_ops @Pure_compose.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_abs <⋆> mbinddt typ F f t <⋆>
   mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
map
  (precompose
     (mbinddt term G (g ◻ allK (incr [ktrm]))))
  (map (ap G)
     (map (precompose (mbinddt typ G g))
        (map (ap G) (pure (pure tm_abs))) <⋆>
      mbinddt typ F f t)) <⋆>
mbinddt term F (f ◻ allK (incr [ktrm])) t0
    rewrite (app_pure_natural).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_abs <⋆> mbinddt typ F f t <⋆>
   mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
map
  (precompose
     (mbinddt term G (g ◻ allK (incr [ktrm]))))
  (map (ap G)
     (map (precompose (mbinddt typ G g))
        (pure (ap G (pure tm_abs))) <⋆>
      mbinddt typ F f t)) <⋆>
mbinddt term F (f ◻ allK (incr [ktrm])) t0
    do 4 rewrite map_ap.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_abs) <⋆> mbinddt typ F f t <⋆>
mbinddt term F (f ◻ allK (incr [ktrm])) t0 =
map
  (compose
     (precompose
        (mbinddt term G (g ◻ allK (incr [ktrm])))))
  (map (compose (ap G))
     (map (precompose (mbinddt typ G g))
        (pure (ap G (pure tm_abs))))) <⋆>
mbinddt typ F f t <⋆>
mbinddt term F (f ◻ allK (incr [ktrm])) t0
    compose near ((pure (F := F) (ap G (pure (F := G) (@tm_abs C))))).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_abs) <⋆> mbinddt typ F f t <⋆>
mbinddt term F (f ◻ allK (incr [ktrm])) t0 =
map
  (compose
     (precompose
        (mbinddt term G (g ◻ allK (incr [ktrm])))))
  ((map (compose (ap G))
    ∘ map (precompose (mbinddt typ G g)))
     (pure (ap G (pure tm_abs)))) <⋆>
mbinddt typ F f t <⋆>
mbinddt term F (f ◻ allK (incr [ktrm])) t0
    rewrite (fun_map_map (F := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_abs) <⋆> mbinddt typ F f t <⋆>
mbinddt term F (f ◻ allK (incr [ktrm])) t0 =
map
  (compose
     (precompose
        (mbinddt term G (g ◻ allK (incr [ktrm])))))
  (map (compose (ap G) ∘ precompose (mbinddt typ G g))
     (pure (ap G (pure tm_abs)))) <⋆>
mbinddt typ F f t <⋆>
mbinddt term F (f ◻ allK (incr [ktrm])) t0
    do 3 rewrite (app_pure_natural).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: typ A
t0: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t0) =
mbinddt term (F ∘ G) (g ⋆dtm f) t0
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
pure (compose (mbinddt term G g) ∘ tm_abs) <⋆>
mbinddt typ F f t <⋆>
mbinddt term F (f ◻ allK (incr [ktrm])) t0 =
pure
  (precompose
     (mbinddt term G (g ◻ allK (incr [ktrm])))
   ∘ (compose (ap G) ∘ precompose (mbinddt typ G g))
       (ap G (pure tm_abs))) <⋆> mbinddt typ F f t <⋆>
mbinddt term F (f ◻ allK (incr [ktrm])) t0
    reflexivity.
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g) (mbinddt term F f (t1 @ t2)) =
mbinddt term (F ∘ G) (g ⋆dtm f) (t1 @ t2) cbn.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_app <⋆> mbinddt term F f t1 <⋆>
   mbinddt term F f t2) =
pure tm_app <⋆> mbinddt term (F ∘ G) (g ⋆dtm f) t1 <⋆>
mbinddt term (F ∘ G) (g ⋆dtm f) t2
    rewrite <- IHt1.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_app <⋆> mbinddt term F f t1 <⋆>
   mbinddt term F f t2) =
pure tm_app <⋆>
map (mbinddt term G g) (mbinddt term F f t1) <⋆>
mbinddt term (F ∘ G) (g ⋆dtm f) t2
    rewrite <- IHt2.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_app <⋆> mbinddt term F f t1 <⋆>
   mbinddt term F f t2) =
pure tm_app <⋆>
map (mbinddt term G g) (mbinddt term F f t1) <⋆>
map (mbinddt term G g) (mbinddt term F f t2)
    do 2 rewrite (ap_compose2 G F).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_app <⋆> mbinddt term F f t1 <⋆>
   mbinddt term F f t2) =
map (ap G)
  (map (ap G) (pure tm_app) <⋆>
   map (mbinddt term G g) (mbinddt term F f t1)) <⋆>
map (mbinddt term G g) (mbinddt term F f t2)
    do 2 rewrite <- (ap_map (G := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_app <⋆> mbinddt term F f t1 <⋆>
   mbinddt term F f t2) =
map (precompose (mbinddt term G g))
  (map (ap G)
     (map (precompose (mbinddt term G g))
        (map (ap G) (pure tm_app)) <⋆>
      mbinddt term F f t1)) <⋆> mbinddt term F f t2
    do 4 rewrite map_ap.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_app) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2 =
map (compose (precompose (mbinddt term G g)))
  (map (compose (ap G))
     (map (precompose (mbinddt term G g))
        (map (ap G) (pure tm_app)))) <⋆>
mbinddt term F f t1 <⋆> mbinddt term F f t2
    compose near (pure (F := F ∘ G) (@tm_app C)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_app) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2 =
map (compose (precompose (mbinddt term G g)))
  (map (compose (ap G))
     ((map (precompose (mbinddt term G g))
       ∘ map (ap G)) (pure tm_app))) <⋆>
mbinddt term F f t1 <⋆> mbinddt term F f t2
    rewrite (fun_map_map (F := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_app) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2 =
map (compose (precompose (mbinddt term G g)))
  (map (compose (ap G))
     (map (precompose (mbinddt term G g) ∘ ap G)
        (pure tm_app))) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2
    compose near (pure (F := F ∘ G) (@tm_app C)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_app) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2 =
map (compose (precompose (mbinddt term G g)))
  ((map (compose (ap G))
    ∘ map (precompose (mbinddt term G g) ∘ ap G))
     (pure tm_app)) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2
    rewrite (fun_map_map (F := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_app) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2 =
map (compose (precompose (mbinddt term G g)))
  (map
     (compose (ap G)
      ∘ (precompose (mbinddt term G g) ∘ ap G))
     (pure tm_app)) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2
    compose near (pure (F := F ∘ G) (@tm_app C)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_app) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2 =
(map (compose (precompose (mbinddt term G g)))
 ∘ map
     (compose (ap G)
      ∘ (precompose (mbinddt term G g) ∘ ap G)))
  (pure tm_app) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2
    rewrite (fun_map_map (F := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_app) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2 =
map
  (compose (precompose (mbinddt term G g))
   ∘ (compose (ap G)
      ∘ (precompose (mbinddt term G g) ∘ ap G)))
  (pure tm_app) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2
    unfold_ops @Pure_compose.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_app) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2 =
map
  (compose (precompose (mbinddt term G g))
   ∘ (compose (ap G)
      ∘ (precompose (mbinddt term G g) ∘ ap G)))
  (pure (pure tm_app)) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2
    do 2 rewrite (app_pure_natural).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t1, t2: term A
IHt1: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t1) =
mbinddt term (F ∘ G) (g ⋆dtm f) t1
IHt2: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t2) =
mbinddt term (F ∘ G) (g ⋆dtm f) t2
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
pure (compose (mbinddt term G g) ∘ tm_app) <⋆>
mbinddt term F f t1 <⋆> mbinddt term F f t2 =
pure
  ((compose (precompose (mbinddt term G g))
    ∘ (compose (ap G)
       ∘ (precompose (mbinddt term G g) ∘ ap G)))
     (pure tm_app)) <⋆> mbinddt term F f t1 <⋆>
mbinddt term F f t2
    reflexivity.
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g) (mbinddt term F f (Λ t)) =
mbinddt term (F ∘ G) (g ⋆dtm f) (Λ t) cbn.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_tab <⋆>
   mbinddt term F (f ◻ allK (incr [ktyp])) t) =
pure tm_tab <⋆>
mbinddt term (F ∘ G) (g ⋆dtm f ◻ allK (incr [ktyp])) t
    setoid_rewrite (compose_dtm_incr_alt).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_tab <⋆>
   mbinddt term F (f ◻ allK (incr [ktyp])) t) =
pure tm_tab <⋆>
mbinddt term (F ∘ G)
  ((g ◻ allK (incr [ktyp]))
   ⋆dtm (f ◻ allK (incr [ktyp]))) t
    rewrite <- IHt.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_tab <⋆>
   mbinddt term F (f ◻ allK (incr [ktyp])) t) =
pure tm_tab <⋆>
map (mbinddt term G (g ◻ allK (incr [ktyp])))
  (mbinddt term F (f ◻ allK (incr [ktyp])) t)
    rewrite (ap_compose2 G F).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_tab <⋆>
   mbinddt term F (f ◻ allK (incr [ktyp])) t) =
map (ap G) (pure tm_tab) <⋆>
map (mbinddt term G (g ◻ allK (incr [ktyp])))
  (mbinddt term F (f ◻ allK (incr [ktyp])) t)
    rewrite <- (ap_map (G := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_tab <⋆>
   mbinddt term F (f ◻ allK (incr [ktyp])) t) =
map
  (precompose
     (mbinddt term G (g ◻ allK (incr [ktyp]))))
  (map (ap G) (pure tm_tab)) <⋆>
mbinddt term F (f ◻ allK (incr [ktyp])) t
    rewrite map_ap.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (mbinddt term G g)) (pure tm_tab) <⋆>
mbinddt term F (f ◻ allK (incr [ktyp])) t =
map
  (precompose
     (mbinddt term G (g ◻ allK (incr [ktyp]))))
  (map (ap G) (pure tm_tab)) <⋆>
mbinddt term F (f ◻ allK (incr [ktyp])) t
    unfold_ops @Pure_compose.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (mbinddt term G g)) (pure tm_tab) <⋆>
mbinddt term F (f ◻ allK (incr [ktyp])) t =
map
  (precompose
     (mbinddt term G (g ◻ allK (incr [ktyp]))))
  (map (ap G) (pure (pure tm_tab))) <⋆>
mbinddt term F (f ◻ allK (incr [ktyp])) t
    do 3 rewrite (app_pure_natural).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
pure (mbinddt term G g ∘ tm_tab) <⋆>
mbinddt term F (f ◻ allK (incr [ktyp])) t =
pure
  (precompose
     (mbinddt term G (g ◻ allK (incr [ktyp])))
     (ap G (pure tm_tab))) <⋆>
mbinddt term F (f ◻ allK (incr [ktyp])) t
    reflexivity.
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g) (mbinddt term F f (t @@ t0)) =
mbinddt term (F ∘ G) (g ⋆dtm f) (t @@ t0) cbn.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_tap <⋆> mbinddt term F f t <⋆>
   bind_type F f t0) =
pure tm_tap <⋆> mbinddt term (F ∘ G) (g ⋆dtm f) t <⋆>
bind_type (F ∘ G) (g ⋆dtm f) t0
    rewrite <- IHt.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_tap <⋆> mbinddt term F f t <⋆>
   bind_type F f t0) =
pure tm_tap <⋆>
map (mbinddt term G g) (mbinddt term F f t) <⋆>
bind_type (F ∘ G) (g ⋆dtm f) t0
    rewrite <- (mbinddt_mbinddt_typ F G).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_tap <⋆> mbinddt term F f t <⋆>
   bind_type F f t0) =
pure tm_tap <⋆>
map (mbinddt term G g) (mbinddt term F f t) <⋆>
(map (mbinddt typ G g) ∘ mbinddt typ F f) t0
    unfold compose at 4.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_tap <⋆> mbinddt term F f t <⋆>
   bind_type F f t0) =
pure tm_tap <⋆>
map (mbinddt term G g) (mbinddt term F f t) <⋆>
map (mbinddt typ G g) (mbinddt typ F f t0)
    do 2 rewrite (ap_compose2 G F).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_tap <⋆> mbinddt term F f t <⋆>
   bind_type F f t0) =
map (ap G)
  (map (ap G) (pure tm_tap) <⋆>
   map (mbinddt term G g) (mbinddt term F f t)) <⋆>
map (mbinddt typ G g) (mbinddt typ F f t0)
    repeat rewrite <- (ap_map (G := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_tap <⋆> mbinddt term F f t <⋆>
   bind_type F f t0) =
map (precompose (mbinddt typ G g))
  (map (ap G)
     (map (precompose (mbinddt term G g))
        (map (ap G) (pure tm_tap)) <⋆>
      mbinddt term F f t)) <⋆> mbinddt typ F f t0
    change (bind_type ?F ?f) with (mbinddt typ F f).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (mbinddt term G g)
  (pure tm_tap <⋆> mbinddt term F f t <⋆>
   mbinddt typ F f t0) =
map (precompose (mbinddt typ G g))
  (map (ap G)
     (map (precompose (mbinddt term G g))
        (map (ap G) (pure tm_tap)) <⋆>
      mbinddt term F f t)) <⋆> mbinddt typ F f t0
    do 4 rewrite map_ap.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_tap) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0 =
map (compose (precompose (mbinddt typ G g)))
  (map (compose (ap G))
     (map (precompose (mbinddt term G g))
        (map (ap G) (pure tm_tap)))) <⋆>
mbinddt term F f t <⋆> mbinddt typ F f t0
    compose near (pure (F := F ∘ G) (@tm_tap C)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_tap) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0 =
map (compose (precompose (mbinddt typ G g)))
  (map (compose (ap G))
     ((map (precompose (mbinddt term G g))
       ∘ map (ap G)) (pure tm_tap))) <⋆>
mbinddt term F f t <⋆> mbinddt typ F f t0
    rewrite (fun_map_map (F := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_tap) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0 =
map (compose (precompose (mbinddt typ G g)))
  (map (compose (ap G))
     (map (precompose (mbinddt term G g) ∘ ap G)
        (pure tm_tap))) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0
    compose near (pure (F := F ∘ G) (@tm_tap C)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_tap) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0 =
map (compose (precompose (mbinddt typ G g)))
  ((map (compose (ap G))
    ∘ map (precompose (mbinddt term G g) ∘ ap G))
     (pure tm_tap)) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0
    rewrite (fun_map_map (F := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_tap) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0 =
map (compose (precompose (mbinddt typ G g)))
  (map
     (compose (ap G)
      ∘ (precompose (mbinddt term G g) ∘ ap G))
     (pure tm_tap)) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0
    compose near (pure (F := F ∘ G) (@tm_tap C)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_tap) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0 =
(map (compose (precompose (mbinddt typ G g)))
 ∘ map
     (compose (ap G)
      ∘ (precompose (mbinddt term G g) ∘ ap G)))
  (pure tm_tap) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0
    rewrite (fun_map_map (F := F)).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_tap) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0 =
map
  (compose (precompose (mbinddt typ G g))
   ∘ (compose (ap G)
      ∘ (precompose (mbinddt term G g) ∘ ap G)))
  (pure tm_tap) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0
    unfold_ops @Pure_compose.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
map (compose (compose (mbinddt term G g)))
  (pure tm_tap) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0 =
map
  (compose (precompose (mbinddt typ G g))
   ∘ (compose (ap G)
      ∘ (precompose (mbinddt term G g) ∘ ap G)))
  (pure (pure tm_tap)) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0
    rewrite (app_pure_natural).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
pure (compose (mbinddt term G g) ∘ tm_tap) <⋆>
mbinddt term F f t <⋆> mbinddt typ F f t0 =
map
  (compose (precompose (mbinddt typ G g))
   ∘ (compose (ap G)
      ∘ (precompose (mbinddt term G g) ∘ ap G)))
  (pure (pure tm_tap)) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0
    rewrite (app_pure_natural).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
B, C, A: Type
t: term A
t0: typ A
IHt: forall
  (g : forall k : K,
       list K2 * B -> G (SystemF k C))
  (f : forall k : K,
       list K2 * A -> F (SystemF k B)),
map (mbinddt term G g) (mbinddt term F f t) =
mbinddt term (F ∘ G) (g ⋆dtm f) t
g: forall k : K, list K2 * B -> G (SystemF k C)
f: forall k : K, list K2 * A -> F (SystemF k B)
H1: Functor F
pure (compose (mbinddt term G g) ∘ tm_tap) <⋆>
mbinddt term F f t <⋆> mbinddt typ F f t0 =
pure
  ((compose (precompose (mbinddt typ G g))
    ∘ (compose (ap G)
       ∘ (precompose (mbinddt term G g) ∘ ap G)))
     (pure tm_tap)) <⋆> mbinddt term F f t <⋆>
mbinddt typ F f t0
    reflexivity.
Qed.

(** ** <<mbinddt_morphism>> *)
(******************************************************************************)

#[local] Set Keyed Unification.

Lemma mbinddt_morphism_typ :
  forall (F : Type -> Type)
    (G : Type -> Type)
    `{ApplicativeMorphism F G ϕ}
    `(f : forall k, list K2 * A -> F (SystemF k B)),
    ϕ (typ B) ∘ mbinddt typ F f =
    mbinddt typ G (fun k => ϕ (SystemF k B) ∘ f k).
forall (F G : Type -> Type) (H : Map F) (H0 : Mult F)
  (H1 : Pure F) (H2 : Map G) (H3 : Mult G)
  (H4 : Pure G) (ϕ : F ⇒ G),
ApplicativeMorphism F G ϕ ->
forall (A B : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
ϕ (typ B) ∘ mbinddt typ F f =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ∘ f k)
Proof.
forall (F G : Type -> Type) (H : Map F) (H0 : Mult F)
  (H1 : Pure F) (H2 : Map G) (H3 : Mult G)
  (H4 : Pure G) (ϕ : F ⇒ G),
ApplicativeMorphism F G ϕ ->
forall (A B : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
ϕ (typ B) ∘ mbinddt typ F f =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ∘ f k)
  intros.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B) ∘ mbinddt typ F f =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ∘ f k) ext t.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
f: forall k : K, list K2 * A -> F (SystemF k B)
t: typ A
(ϕ (typ B) ∘ mbinddt typ F f) t =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ∘ f k) t generalize dependent f.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
forall
  f : forall k : K, list K2 * A -> F (SystemF k B),
(ϕ (typ B) ∘ mbinddt typ F f) t =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ∘ f k) t unfold compose.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
forall
  f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t) =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ○ f k) t induction t; intro f.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
b: base_typ
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B) (mbinddt typ F f (ty_c b)) =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ○ f k)
  (ty_c b)
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
v: A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B) (mbinddt typ F f (ty_v v)) =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ○ f k)
  (ty_v v)
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: typ A
IHt1: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t1) =
mbinddt typ G
  (fun k : K => ϕ (SystemF k B) ○ f k) t1
IHt2: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t2) =
mbinddt typ G
  (fun k : K => ϕ (SystemF k B) ○ f k) t2
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B) (mbinddt typ F f (t1 ⟹ t2)) =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ○ f k)
  (t1 ⟹ t2)
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
IHt: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t) =
mbinddt typ G
  (fun k : K => ϕ (SystemF k B) ○ f k) t
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B) (mbinddt typ F f (∀ t)) =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ○ f k)
  (∀ t)
  -
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
b: base_typ
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B) (mbinddt typ F f (ty_c b)) =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ○ f k)
  (ty_c b) cbn.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
b: base_typ
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B) (pure (ty_c b)) = pure (ty_c b) rewrite (appmor_pure).
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
b: base_typ
f: forall k : K, list K2 * A -> F (SystemF k B)
pure (ty_c b) = pure (ty_c b) reflexivity.
  -
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
v: A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B) (mbinddt typ F f (ty_v v)) =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ○ f k)
  (ty_v v) reflexivity.
  -
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: typ A
IHt1: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t1) =
mbinddt typ G
  (fun k : K => ϕ (SystemF k B) ○ f k) t1
IHt2: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t2) =
mbinddt typ G
  (fun k : K => ϕ (SystemF k B) ○ f k) t2
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B) (mbinddt typ F f (t1 ⟹ t2)) =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ○ f k)
  (t1 ⟹ t2) cbn.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: typ A
IHt1: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t1) =
mbinddt typ G
  (fun k : K => ϕ (SystemF k B) ○ f k) t1
IHt2: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t2) =
mbinddt typ G
  (fun k : K => ϕ (SystemF k B) ○ f k) t2
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B)
  (pure ty_ar <⋆> mbinddt typ F f t1 <⋆>
   mbinddt typ F f t2) =
pure ty_ar <⋆>
mbinddt typ G (fun k : K2 => ϕ (SystemF k B) ○ f k) t1 <⋆>
mbinddt typ G (fun k : K2 => ϕ (SystemF k B) ○ f k) t2
    rewrite <- IHt1.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: typ A
IHt1: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t1) =
mbinddt typ G
  (fun k : K => ϕ (SystemF k B) ○ f k) t1
IHt2: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t2) =
mbinddt typ G
  (fun k : K => ϕ (SystemF k B) ○ f k) t2
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B)
  (pure ty_ar <⋆> mbinddt typ F f t1 <⋆>
   mbinddt typ F f t2) =
pure ty_ar <⋆> ϕ (typ B) (mbinddt typ F f t1) <⋆>
mbinddt typ G (fun k : K2 => ϕ (SystemF k B) ○ f k) t2 clear IHt1.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: typ A
IHt2: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t2) =
mbinddt typ G
  (fun k : K => ϕ (SystemF k B) ○ f k) t2
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B)
  (pure ty_ar <⋆> mbinddt typ F f t1 <⋆>
   mbinddt typ F f t2) =
pure ty_ar <⋆> ϕ (typ B) (mbinddt typ F f t1) <⋆>
mbinddt typ G (fun k : K2 => ϕ (SystemF k B) ○ f k) t2
    rewrite <- IHt2.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: typ A
IHt2: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t2) =
mbinddt typ G
  (fun k : K => ϕ (SystemF k B) ○ f k) t2
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B)
  (pure ty_ar <⋆> mbinddt typ F f t1 <⋆>
   mbinddt typ F f t2) =
pure ty_ar <⋆> ϕ (typ B) (mbinddt typ F f t1) <⋆>
ϕ (typ B) (mbinddt typ F f t2) clear IHt2.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: typ A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B)
  (pure ty_ar <⋆> mbinddt typ F f t1 <⋆>
   mbinddt typ F f t2) =
pure ty_ar <⋆> ϕ (typ B) (mbinddt typ F f t1) <⋆>
ϕ (typ B) (mbinddt typ F f t2)
    rewrite ap_morphism_1.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: typ A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B -> typ B) (pure ty_ar <⋆> mbinddt typ F f t1) <⋆>
ϕ (typ B) (mbinddt typ F f t2) =
pure ty_ar <⋆> ϕ (typ B) (mbinddt typ F f t1) <⋆>
ϕ (typ B) (mbinddt typ F f t2)
    rewrite ap_morphism_1.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: typ A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B -> typ B -> typ B) (pure ty_ar) <⋆>
ϕ (typ B) (mbinddt typ F f t1) <⋆>
ϕ (typ B) (mbinddt typ F f t2) =
pure ty_ar <⋆> ϕ (typ B) (mbinddt typ F f t1) <⋆>
ϕ (typ B) (mbinddt typ F f t2)
    rewrite (appmor_pure).
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: typ A
f: forall k : K, list K2 * A -> F (SystemF k B)
pure ty_ar <⋆> ϕ (typ B) (mbinddt typ F f t1) <⋆>
ϕ (typ B) (mbinddt typ F f t2) =
pure ty_ar <⋆> ϕ (typ B) (mbinddt typ F f t1) <⋆>
ϕ (typ B) (mbinddt typ F f t2)
    reflexivity.
  -
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
IHt: forall f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t) =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ○ f k) t
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B) (mbinddt typ F f (∀ t)) =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ○ f k)
  (∀ t) cbn.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
IHt: forall f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t) =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ○ f k) t
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B)
  (pure ty_univ <⋆>
   mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
pure ty_univ <⋆>
mbinddt typ G
  ((fun k : K2 => ϕ (SystemF k B) ○ f k)
   ◻ allK (incr [ktyp])) t
    rewrite <- IHt.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
IHt: forall f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (typ B) (mbinddt typ F f t) =
mbinddt typ G (fun k : K => ϕ (SystemF k B) ○ f k) t
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B)
  (pure ty_univ <⋆>
   mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
pure ty_univ <⋆>
ϕ (typ B)
  (mbinddt typ F
     (fun k : K => f k ○ allK (incr [ktyp]) k) t) clear IHt.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B)
  (pure ty_univ <⋆>
   mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
pure ty_univ <⋆>
ϕ (typ B)
  (mbinddt typ F
     (fun k : K => f k ○ allK (incr [ktyp]) k) t)
    rewrite ap_morphism_1.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B -> typ B) (pure ty_univ) <⋆>
ϕ (typ B) (mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
pure ty_univ <⋆>
ϕ (typ B)
  (mbinddt typ F
     (fun k : K => f k ○ allK (incr [ktyp]) k) t)
    rewrite (appmor_pure).
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
f: forall k : K, list K2 * A -> F (SystemF k B)
pure ty_univ <⋆>
ϕ (typ B) (mbinddt typ F (f ◻ allK (incr [ktyp])) t) =
pure ty_univ <⋆>
ϕ (typ B)
  (mbinddt typ F
     (fun k : K => f k ○ allK (incr [ktyp]) k) t)
    reflexivity.
Qed.

Lemma mbinddt_morphism_term :
  forall (F : Type -> Type)
    (G : Type -> Type)
    `{ApplicativeMorphism F G ϕ}
    `(f : forall k, list K2 * A -> F (SystemF k B)),
    ϕ (term B) ∘ mbinddt term F f =
    mbinddt term G (fun k => ϕ (SystemF k B) ∘ f k).
forall (F G : Type -> Type) (H : Map F) (H0 : Mult F)
  (H1 : Pure F) (H2 : Map G) (H3 : Mult G)
  (H4 : Pure G) (ϕ : F ⇒ G),
ApplicativeMorphism F G ϕ ->
forall (A B : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
ϕ (term B) ∘ mbinddt term F f =
mbinddt term G (fun k : K => ϕ (SystemF k B) ∘ f k)
Proof.
forall (F G : Type -> Type) (H : Map F) (H0 : Mult F)
  (H1 : Pure F) (H2 : Map G) (H3 : Mult G)
  (H4 : Pure G) (ϕ : F ⇒ G),
ApplicativeMorphism F G ϕ ->
forall (A B : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
ϕ (term B) ∘ mbinddt term F f =
mbinddt term G (fun k : K => ϕ (SystemF k B) ∘ f k)
  intros.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B) ∘ mbinddt term F f =
mbinddt term G (fun k : K => ϕ (SystemF k B) ∘ f k) ext t.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
f: forall k : K, list K2 * A -> F (SystemF k B)
t: term A
(ϕ (term B) ∘ mbinddt term F f) t =
mbinddt term G (fun k : K => ϕ (SystemF k B) ∘ f k) t generalize dependent f.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
forall
  f : forall k : K, list K2 * A -> F (SystemF k B),
(ϕ (term B) ∘ mbinddt term F f) t =
mbinddt term G (fun k : K => ϕ (SystemF k B) ∘ f k) t unfold compose.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
forall
  f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k) t induction t; intro f.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
v: A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B) (mbinddt term F f (tm_var v)) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k)
  (tm_var v)
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
t0: term A
IHt: forall f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t0) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k) t0
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B) (mbinddt term F f (λ t ⋅ t0)) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k)
  (λ t ⋅ t0)
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: term A
IHt1: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t1) =
mbinddt term G
  (fun k : K => ϕ (SystemF k B) ○ f k) t1
IHt2: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t2) =
mbinddt term G
  (fun k : K => ϕ (SystemF k B) ○ f k) t2
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B) (mbinddt term F f (t1 @ t2)) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k)
  (t1 @ t2)
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
IHt: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t) =
mbinddt term G
  (fun k : K => ϕ (SystemF k B) ○ f k) t
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B) (mbinddt term F f (Λ t)) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k)
  (Λ t)
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
t0: typ A
IHt: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t) =
mbinddt term G
  (fun k : K => ϕ (SystemF k B) ○ f k) t
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B) (mbinddt term F f (t @@ t0)) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k)
  (t @@ t0)
  -
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
v: A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B) (mbinddt term F f (tm_var v)) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k)
  (tm_var v) reflexivity.
  -
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
t0: term A
IHt: forall f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t0) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k) t0
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B) (mbinddt term F f (λ t ⋅ t0)) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k)
  (λ t ⋅ t0) cbn.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
t0: term A
IHt: forall f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t0) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k) t0
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B)
  (pure tm_abs <⋆> bind_type F f t <⋆>
   mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
pure tm_abs <⋆>
bind_type G (fun k : K2 => ϕ (SystemF k B) ○ f k) t <⋆>
mbinddt term G
  ((fun k : K2 => ϕ (SystemF k B) ○ f k)
   ◻ allK (incr [ktrm])) t0
    rewrite <- IHt.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
t0: term A
IHt: forall f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t0) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k) t0
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B)
  (pure tm_abs <⋆> bind_type F f t <⋆>
   mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
pure tm_abs <⋆>
bind_type G (fun k : K2 => ϕ (SystemF k B) ○ f k) t <⋆>
ϕ (term B)
  (mbinddt term F
     (fun k : K => f k ○ allK (incr [ktrm]) k) t0) clear IHt.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
t0: term A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B)
  (pure tm_abs <⋆> bind_type F f t <⋆>
   mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
pure tm_abs <⋆>
bind_type G (fun k : K2 => ϕ (SystemF k B) ○ f k) t <⋆>
ϕ (term B)
  (mbinddt term F
     (fun k : K => f k ○ allK (incr [ktrm]) k) t0)
    do 2 rewrite ap_morphism_1.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
t0: term A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (typ B -> term B -> term B) (pure tm_abs) <⋆>
ϕ (typ B) (bind_type F f t) <⋆>
ϕ (term B)
  (mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
pure tm_abs <⋆>
bind_type G (fun k : K2 => ϕ (SystemF k B) ○ f k) t <⋆>
ϕ (term B)
  (mbinddt term F
     (fun k : K => f k ○ allK (incr [ktrm]) k) t0)
    rewrite (appmor_pure).
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
t0: term A
f: forall k : K, list K2 * A -> F (SystemF k B)
pure tm_abs <⋆> ϕ (typ B) (bind_type F f t) <⋆>
ϕ (term B)
  (mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
pure tm_abs <⋆>
bind_type G (fun k : K2 => ϕ (SystemF k B) ○ f k) t <⋆>
ϕ (term B)
  (mbinddt term F
     (fun k : K => f k ○ allK (incr [ktrm]) k) t0)
    change (bind_type ?F ?f) with (mbinddt typ F f).
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
t0: term A
f: forall k : K, list K2 * A -> F (SystemF k B)
pure tm_abs <⋆> ϕ (typ B) (mbinddt typ F f t) <⋆>
ϕ (term B)
  (mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
pure tm_abs <⋆>
mbinddt typ G (fun k : K2 => ϕ (SystemF k B) ○ f k) t <⋆>
ϕ (term B)
  (mbinddt term F
     (fun k : K => f k ○ allK (incr [ktrm]) k) t0)
    compose near t on left.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
t0: term A
f: forall k : K, list K2 * A -> F (SystemF k B)
pure tm_abs <⋆> (ϕ (typ B) ∘ mbinddt typ F f) t <⋆>
ϕ (term B)
  (mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
pure tm_abs <⋆>
mbinddt typ G (fun k : K2 => ϕ (SystemF k B) ○ f k) t <⋆>
ϕ (term B)
  (mbinddt term F
     (fun k : K => f k ○ allK (incr [ktrm]) k) t0)
    rewrite (mbinddt_morphism_typ F G).
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: typ A
t0: term A
f: forall k : K, list K2 * A -> F (SystemF k B)
pure tm_abs <⋆>
mbinddt typ G (fun k : K => ϕ (SystemF k B) ∘ f k) t <⋆>
ϕ (term B)
  (mbinddt term F (f ◻ allK (incr [ktrm])) t0) =
pure tm_abs <⋆>
mbinddt typ G (fun k : K2 => ϕ (SystemF k B) ○ f k) t <⋆>
ϕ (term B)
  (mbinddt term F
     (fun k : K => f k ○ allK (incr [ktrm]) k) t0)
    reflexivity.
  -
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: term A
IHt1: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t1) =
mbinddt term G
  (fun k : K => ϕ (SystemF k B) ○ f k) t1
IHt2: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t2) =
mbinddt term G
  (fun k : K => ϕ (SystemF k B) ○ f k) t2
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B) (mbinddt term F f (t1 @ t2)) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k)
  (t1 @ t2) cbn.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: term A
IHt1: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t1) =
mbinddt term G
  (fun k : K => ϕ (SystemF k B) ○ f k) t1
IHt2: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t2) =
mbinddt term G
  (fun k : K => ϕ (SystemF k B) ○ f k) t2
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B)
  (pure tm_app <⋆> mbinddt term F f t1 <⋆>
   mbinddt term F f t2) =
pure tm_app <⋆>
mbinddt term G (fun k : K2 => ϕ (SystemF k B) ○ f k)
  t1 <⋆>
mbinddt term G (fun k : K2 => ϕ (SystemF k B) ○ f k)
  t2
    rewrite <- IHt1.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: term A
IHt1: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t1) =
mbinddt term G
  (fun k : K => ϕ (SystemF k B) ○ f k) t1
IHt2: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t2) =
mbinddt term G
  (fun k : K => ϕ (SystemF k B) ○ f k) t2
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B)
  (pure tm_app <⋆> mbinddt term F f t1 <⋆>
   mbinddt term F f t2) =
pure tm_app <⋆> ϕ (term B) (mbinddt term F f t1) <⋆>
mbinddt term G (fun k : K2 => ϕ (SystemF k B) ○ f k)
  t2 clear IHt1.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: term A
IHt2: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t2) =
mbinddt term G
  (fun k : K => ϕ (SystemF k B) ○ f k) t2
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B)
  (pure tm_app <⋆> mbinddt term F f t1 <⋆>
   mbinddt term F f t2) =
pure tm_app <⋆> ϕ (term B) (mbinddt term F f t1) <⋆>
mbinddt term G (fun k : K2 => ϕ (SystemF k B) ○ f k)
  t2
    rewrite <- IHt2.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: term A
IHt2: forall
  f : forall k : K,
      list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t2) =
mbinddt term G
  (fun k : K => ϕ (SystemF k B) ○ f k) t2
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B)
  (pure tm_app <⋆> mbinddt term F f t1 <⋆>
   mbinddt term F f t2) =
pure tm_app <⋆> ϕ (term B) (mbinddt term F f t1) <⋆>
ϕ (term B) (mbinddt term F f t2) clear IHt2.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: term A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B)
  (pure tm_app <⋆> mbinddt term F f t1 <⋆>
   mbinddt term F f t2) =
pure tm_app <⋆> ϕ (term B) (mbinddt term F f t1) <⋆>
ϕ (term B) (mbinddt term F f t2)
    rewrite ap_morphism_1.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: term A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B -> term B)
  (pure tm_app <⋆> mbinddt term F f t1) <⋆>
ϕ (term B) (mbinddt term F f t2) =
pure tm_app <⋆> ϕ (term B) (mbinddt term F f t1) <⋆>
ϕ (term B) (mbinddt term F f t2)
    rewrite ap_morphism_1.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: term A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B -> term B -> term B) (pure tm_app) <⋆>
ϕ (term B) (mbinddt term F f t1) <⋆>
ϕ (term B) (mbinddt term F f t2) =
pure tm_app <⋆> ϕ (term B) (mbinddt term F f t1) <⋆>
ϕ (term B) (mbinddt term F f t2)
    rewrite (appmor_pure).
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t1, t2: term A
f: forall k : K, list K2 * A -> F (SystemF k B)
pure tm_app <⋆> ϕ (term B) (mbinddt term F f t1) <⋆>
ϕ (term B) (mbinddt term F f t2) =
pure tm_app <⋆> ϕ (term B) (mbinddt term F f t1) <⋆>
ϕ (term B) (mbinddt term F f t2)
    reflexivity.
  -
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
IHt: forall f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k) t
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B) (mbinddt term F f (Λ t)) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k)
  (Λ t) cbn.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
IHt: forall f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k) t
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B)
  (pure tm_tab <⋆>
   mbinddt term F (f ◻ allK (incr [ktyp])) t) =
pure tm_tab <⋆>
mbinddt term G
  ((fun k : K2 => ϕ (SystemF k B) ○ f k)
   ◻ allK (incr [ktyp])) t
    rewrite <- IHt.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
IHt: forall f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k) t
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B)
  (pure tm_tab <⋆>
   mbinddt term F (f ◻ allK (incr [ktyp])) t) =
pure tm_tab <⋆>
ϕ (term B)
  (mbinddt term F
     (fun k : K => f k ○ allK (incr [ktyp]) k) t) clear IHt.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B)
  (pure tm_tab <⋆>
   mbinddt term F (f ◻ allK (incr [ktyp])) t) =
pure tm_tab <⋆>
ϕ (term B)
  (mbinddt term F
     (fun k : K => f k ○ allK (incr [ktyp]) k) t)
    rewrite ap_morphism_1.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B -> term B) (pure tm_tab) <⋆>
ϕ (term B) (mbinddt term F (f ◻ allK (incr [ktyp])) t) =
pure tm_tab <⋆>
ϕ (term B)
  (mbinddt term F
     (fun k : K => f k ○ allK (incr [ktyp]) k) t)
    rewrite (appmor_pure).
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
f: forall k : K, list K2 * A -> F (SystemF k B)
pure tm_tab <⋆>
ϕ (term B) (mbinddt term F (f ◻ allK (incr [ktyp])) t) =
pure tm_tab <⋆>
ϕ (term B)
  (mbinddt term F
     (fun k : K => f k ○ allK (incr [ktyp]) k) t)
    reflexivity.
  -
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
t0: typ A
IHt: forall f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k) t
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B) (mbinddt term F f (t @@ t0)) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k)
  (t @@ t0) cbn.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
t0: typ A
IHt: forall f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k) t
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B)
  (pure tm_tap <⋆> mbinddt term F f t <⋆>
   bind_type F f t0) =
pure tm_tap <⋆>
mbinddt term G (fun k : K2 => ϕ (SystemF k B) ○ f k) t <⋆>
bind_type G (fun k : K2 => ϕ (SystemF k B) ○ f k) t0
    rewrite <- IHt.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
t0: typ A
IHt: forall f : forall k : K, list K2 * A -> F (SystemF k B),
ϕ (term B) (mbinddt term F f t) =
mbinddt term G (fun k : K => ϕ (SystemF k B) ○ f k) t
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B)
  (pure tm_tap <⋆> mbinddt term F f t <⋆>
   bind_type F f t0) =
pure tm_tap <⋆> ϕ (term B) (mbinddt term F f t) <⋆>
bind_type G (fun k : K2 => ϕ (SystemF k B) ○ f k) t0 clear IHt.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
t0: typ A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B)
  (pure tm_tap <⋆> mbinddt term F f t <⋆>
   bind_type F f t0) =
pure tm_tap <⋆> ϕ (term B) (mbinddt term F f t) <⋆>
bind_type G (fun k : K2 => ϕ (SystemF k B) ○ f k) t0
    do 2 rewrite ap_morphism_1.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
t0: typ A
f: forall k : K, list K2 * A -> F (SystemF k B)
ϕ (term B -> typ B -> term B) (pure tm_tap) <⋆>
ϕ (term B) (mbinddt term F f t) <⋆>
ϕ (typ B) (bind_type F f t0) =
pure tm_tap <⋆> ϕ (term B) (mbinddt term F f t) <⋆>
bind_type G (fun k : K2 => ϕ (SystemF k B) ○ f k) t0
    rewrite (appmor_pure).
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
t0: typ A
f: forall k : K, list K2 * A -> F (SystemF k B)
pure tm_tap <⋆> ϕ (term B) (mbinddt term F f t) <⋆>
ϕ (typ B) (bind_type F f t0) =
pure tm_tap <⋆> ϕ (term B) (mbinddt term F f t) <⋆>
bind_type G (fun k : K2 => ϕ (SystemF k B) ○ f k) t0
    change (bind_type ?F ?f) with (mbinddt typ F f).
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
t0: typ A
f: forall k : K, list K2 * A -> F (SystemF k B)
pure tm_tap <⋆> ϕ (term B) (mbinddt term F f t) <⋆>
ϕ (typ B) (mbinddt typ F f t0) =
pure tm_tap <⋆> ϕ (term B) (mbinddt term F f t) <⋆>
mbinddt typ G (fun k : K2 => ϕ (SystemF k B) ○ f k) t0
    compose near t0 on left.
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
t0: typ A
f: forall k : K, list K2 * A -> F (SystemF k B)
pure tm_tap <⋆> ϕ (term B) (mbinddt term F f t) <⋆>
(ϕ (typ B) ∘ mbinddt typ F f) t0 =
pure tm_tap <⋆> ϕ (term B) (mbinddt term F f t) <⋆>
mbinddt typ G (fun k : K2 => ϕ (SystemF k B) ○ f k) t0
    rewrite (mbinddt_morphism_typ F G).
F, G: Type -> Type
H: Map F
H0: Mult F
H1: Pure F
H2: Map G
H3: Mult G
H4: Pure G
ϕ: F ⇒ G
H5: ApplicativeMorphism F G ϕ
A, B: Type
t: term A
t0: typ A
f: forall k : K, list K2 * A -> F (SystemF k B)
pure tm_tap <⋆> ϕ (term B) (mbinddt term F f t) <⋆>
mbinddt typ G (fun k : K => ϕ (SystemF k B) ∘ f k) t0 =
pure tm_tap <⋆> ϕ (term B) (mbinddt term F f t) <⋆>
mbinddt typ G (fun k : K2 => ϕ (SystemF k B) ○ f k) t0
    reflexivity.
Qed.

#[local] Unset Keyed Unification.

(** ** <<mbinddt_comp_mret>> *)
(******************************************************************************)
Lemma mbinddt_comp_mret_typ :
  forall (F : Type -> Type)
    `{Applicative F}
    `(f : forall k, list K2 * A -> F (SystemF k B)),
    mbinddt typ F f ∘ mret SystemF ktyp = f ktyp ∘ pair nil.
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
mbinddt typ F f ∘ mret SystemF ktyp = f ktyp ∘ pair []
Proof.
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
mbinddt typ F f ∘ mret SystemF ktyp = f ktyp ∘ pair []
  reflexivity.
Qed.

Lemma mbinddt_comp_mret_term :
  forall (F : Type -> Type)
    `{Applicative F}
    `(f : forall k, list K2 * A -> F (SystemF k B)),
    mbinddt term F f ∘ mret SystemF ktrm = f ktrm ∘ pair nil.
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
mbinddt term F f ∘ mret SystemF ktrm =
f ktrm ∘ pair []
Proof.
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
mbinddt term F f ∘ mret SystemF ktrm =
f ktrm ∘ pair []
  reflexivity.
Qed.

Corollary mbinddt_comp_mret_F :
  forall k F `{Applicative F}
    `(f : forall k, (list K2) * A -> F (SystemF k B)),
    mbinddt (W := list K2) (T := SystemF) (SystemF k) F f ∘ mret SystemF k = (fun a => f k (Ƶ, a)).
forall (k : K) (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type)
  (f : forall k0 : K, list K2 * A -> F (SystemF k0 B)),
mbinddt (SystemF k) F f ∘ mret SystemF k =
f k ○ pair Ƶ
Proof.
forall (k : K) (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type)
  (f : forall k0 : K, list K2 * A -> F (SystemF k0 B)),
mbinddt (SystemF k) F f ∘ mret SystemF k =
f k ○ pair Ƶ
  intro k.
k: K
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
mbinddt (SystemF k) F f ∘ mret SystemF k =
f k ○ pair Ƶ destruct k.
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
mbinddt (SystemF ktyp) F f ∘ mret SystemF ktyp =
f ktyp ○ pair Ƶ
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
mbinddt (SystemF ktrm) F f ∘ mret SystemF ktrm =
f ktrm ○ pair Ƶ
  -
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
mbinddt (SystemF ktyp) F f ∘ mret SystemF ktyp =
f ktyp ○ pair Ƶ apply mbinddt_comp_mret_typ.
  -
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type)
  (f : forall k : K, list K2 * A -> F (SystemF k B)),
mbinddt (SystemF ktrm) F f ∘ mret SystemF ktrm =
f ktrm ○ pair Ƶ apply mbinddt_comp_mret_term.
Qed.

(** ** <<DTPreModule>> instances *)
(******************************************************************************)
#[export] Instance DTP_typ: MultiDecoratedTraversablePreModule
                              (list K2) SystemF typ :=
  {| dtp_mbinddt_mret := @mbinddt_mret_typ;
     dtp_mbinddt_mbinddt := @mbinddt_mbinddt_typ;
     dtp_mbinddt_morphism := @mbinddt_morphism_typ;
  |}.

#[export] Instance DTP_term: MultiDecoratedTraversablePreModule
                               (list K2) SystemF term :=
  {| dtp_mbinddt_mret := @mbinddt_mret_term;
     dtp_mbinddt_mbinddt := @mbinddt_mbinddt_term;
     dtp_mbinddt_morphism := @mbinddt_morphism_term;
  |}.

#[export] Instance: forall k, MultiDecoratedTraversablePreModule
                           (list K2) SystemF (SystemF k) :=
  fun k => match k with
        | ktyp => DTP_typ
        | ktrm => DTP_term
        end.

#[export] Instance: MultiDecoratedTraversableMonad (list K2) SystemF :=
  {| dtm_mbinddt_comp_mret := mbinddt_comp_mret_F;
  |}.

(** * System F type system and operational rules *)
(******************************************************************************)
Reserved Notation "Δ ; Γ ⊢ t : τ" (at level 90, t at level 99).

(** ** Contexts and well-formedness predicates *)
(******************************************************************************)

(** *** Context of type variables *)
Definition kind_ctx := alist unit.

(** *** Context of term variables *)
Definition type_ctx := alist (typ LN).

(** *** Well-formedness for kinding contexts *)
(** A kinding context is well-formed when its keys, i.e. type
    variables, are unique. *)
Definition ok_kind_ctx : kind_ctx -> Prop := uniq.

#[export] Hint Unfold ok_kind_ctx : tea_alist.

(** *** Well-formedness of type expressions in a kinding context *)
(** A type is well-formed in a kinding context <<Δ>> when all of its
    type variables appear in Δ and the type is locally closed. *)
Definition ok_type : kind_ctx -> typ LN -> Prop :=
  fun Δ τ => scoped typ ktyp τ (domset Δ) /\ LC typ ktyp τ.

(** *** Well-formedness for typing contexts *)
(** A typing context <<Γ>> is well-formed in kinding context <<Δ>>
    when the keys of <<Γ>> (i.e. term variables) are unique, and each
    associated type is itself well-formed in context <<Δ>>. *)
Definition ok_type_ctx : kind_ctx -> type_ctx -> Prop :=
  fun Δ Γ => uniq Γ /\ forall τ, τ ∈ range Γ -> ok_type Δ τ.

(** *** Well-formedness of term expressions in context *)
(** A term <<t>> is well-formed in contexts <<Δ>> and <<Γ>> when its
    type variables are declared in <<Δ>>, its term variables are
    declared in <<Γ>>, and it is locally closed with respect to both
    kinds of variables. *)
Definition ok_term : kind_ctx -> type_ctx -> term LN -> Prop :=
  fun Δ Γ t => scoped term ktyp t (domset Δ) /\
            scoped term ktrm t (domset Γ) /\
            LC term ktrm t /\
            LC term ktyp t.

(** ** Typing judgments *)
(******************************************************************************)
Implicit Types (Δ : kind_ctx) (Γ : type_ctx) (τ : typ LN).

Inductive Judgment : kind_ctx -> type_ctx -> term LN -> typ LN -> Prop :=
| j_var :
    forall Δ Γ x τ,
      ok_kind_ctx Δ ->
      ok_type_ctx Δ Γ ->
      (x, τ) ∈ (Γ : list (atom * typ LN)) ->
      (Δ ; Γ ⊢ tm_var (Fr x) : τ)
| j_abs :
    forall Δ Γ (L:AtomSet.t) t τ1 τ2,
      (forall x, x `notin` L  ->
            Δ ; Γ ++ x ~ τ1 ⊢ open term ktrm (tm_var (Fr x)) t : τ2) ->
      (Δ ; Γ ⊢ tm_abs τ1 t : ty_ar τ1 τ2)
| j_app :
    forall Δ Γ t1 t2 τ1 τ2,
      (Δ ; Γ ⊢ t1 : ty_ar τ1 τ2) ->
      (Δ ; Γ ⊢ t2 : τ1) ->
      (Δ ; Γ ⊢ tm_app t1 t2 : τ2)
| j_univ :
    forall Δ Γ L τ t,
      (forall x, x `notin` L ->
            Δ ++ x ~ tt ; Γ ⊢ open term ktyp (ty_v (Fr x)) t
                          : open typ ktyp (ty_v (Fr x)) τ) ->
      (Δ ; Γ ⊢ tm_tab t : ty_univ τ)
| j_inst :
    forall Δ Γ t τ1 τ2,
      ok_type Δ τ1 ->
      (Δ ; Γ ⊢ t : ty_univ τ2) ->
      (Δ ; Γ ⊢ tm_tap t τ1 : open typ ktyp τ1 τ2)
where "Δ ; Γ ⊢ t : τ" := (Judgment Δ Γ t τ).

(** ** Values and reduction rules *)
(******************************************************************************)
Inductive value : term LN -> Prop :=
| val_abs : forall T t, value (tm_abs T t)
| val_tab : forall t, value (tm_tab t).

Inductive red : term LN -> term LN -> Prop :=
| red_app_l : forall t1 t1' t2,
    red t1 t1' ->
    red (tm_app t1 t2) (tm_app t1' t2)
| red_app_r : forall t1 t2 t2',
    value t1 ->
    red t2 t2' ->
    red (tm_app t1 t2) (tm_app t1 t2')
| red_abs : forall T t1 t2,
    value t2 ->
    red (tm_app (tm_abs T t1) t2) (open term ktrm t2 t1)
| red_tapl : forall t t' T,
    red t t' ->
    red (tm_tap t T) (tm_tap t' T)
| red_tab : forall T t,
    red (tm_tap (tm_tab t) T) (open term ktyp T t).

Definition preservation := forall t t' τ,
    (nil ; nil ⊢ t : τ) ->
    red t t' ->
    (nil ; nil ⊢ t' : τ).

Definition progress := forall t τ,
    (nil ; nil ⊢ t : τ) ->
    value t \/ exists t', red t t'.