Formalizing variadic syntax with Tealeaves

let with telescoping semantics

From Tealeaves Require Export
  Examples.VariadicLet.Terms
  Functors.List_Telescoping
  Adapters.Compositions.DecoratedTraversableModule.

#[local] Generalizable Variables G A B C.
#[local] Set Implicit Arguments.
#[local] Open Scope nat_scope.

Fixpoint binddt_term
  (G : Type -> Type) `{Map G} `{Pure G} `{Mult G}
  {v1 v2 : Type}
  (f : nat * v1 -> G (term v2))
  (t : term v1) : G (term v2) :=
  match t with
  | tvar v => f (0, v)
  | abs body => pure (@abs v2) <⋆> binddt_term (f ⦿ 1) body
  | letin defs body =>
      pure (@letin v2) <⋆>
        ((fix F acc ls :=
            match ls with
            | nil => pure nil
            | cons d0 drest =>
                pure cons <⋆> binddt_term (f ⦿ acc) d0 <⋆> F (S acc) drest
            end) 0 defs) <⋆> binddt_term (f ⦿ length defs) body
  | app t1 t2 =>
      pure (@app v2) <⋆> binddt_term f t1 <⋆> binddt_term f t2
  end.

#[export] Instance Binddt_term: Binddt nat term term := @binddt_term.

#[export] Instance Map_term: Map term
  := DerivedOperations.Map_Binddt nat term term.
#[export] Instance Mapd_term: Mapd nat term
  := DerivedOperations.Mapd_Binddt nat term term.
#[export] Instance Traverse_term: Traverse term
  := DerivedOperations.Traverse_Binddt nat term term.
#[export] Instance Mapdt_term: Mapdt nat term
  := DerivedOperations.Mapdt_Binddt nat term term.
#[export] Instance Bind_term: Bind term term
  := DerivedOperations.Bind_Binddt nat term term.
#[export] Instance Bindd_term: Bindd nat term term
  := DerivedOperations.Bindd_Binddt nat term term.
#[export] Instance Bindt_term: Bindt term term
  := DerivedOperations.Bindt_Binddt nat term term.
#[export] Instance ToSubset_term: ToSubset term
  := ToSubset_Traverse.
#[export] Instance ToBatch_term: ToBatch term
  := DerivedOperations.ToBatch_Traverse.
#[export] Instance ToBatch3_term: ToBatch3 nat term
  := DerivedOperations.ToBatch3_Mapdt.

Definition subst_in_defs
  `{Applicative G} {v1 v2 : Type}
  (f : nat * v1 -> G (term v2)):
  list (term v1) -> G (list (term v2)) :=
  binddt (Binddt := Mapdt_Binddt_compose (Mapdt_F := Mapdt_Telescoping_List))
    (U := list ∘ term) f.

Section rewriting.

  Section pointful.

    Context
      `{Applicative G} (v1 v2 : Type)
        (f : nat * v1 -> G (term v2)).

    Lemma binddt_term_rw1: forall (v: v1),
        binddt f (tvar v) = f (Ƶ, v).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall v : v1, binddt f (tvar v) = f (Ƶ, v)
    Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall v : v1, binddt f (tvar v) = f (Ƶ, v)
      reflexivity.
    Qed.

    Lemma binddt_term_rw2: forall (t: term v1),
        binddt f (abs t) =
          pure (@abs v2) <⋆> binddt (f ⦿ 1) t.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall t : term v1,
binddt f (abs t) =
pure (abs (v:=v2)) <⋆> binddt (f ⦿ 1) t
    Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall t : term v1,
binddt f (abs t) =
pure (abs (v:=v2)) <⋆> binddt (f ⦿ 1) t
      reflexivity.
    Qed.

    Lemma binddt_term_rw3: forall (l : list (term v1)) (body: term v1),
        binddt f (letin l body) =
          pure (@letin v2) <⋆> subst_in_defs f l <⋆>
            binddt (f ⦿ length l) body.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall (l : list (term v1)) (body : term v1),
binddt f (letin l body) =
pure (letin (v:=v2)) <⋆> subst_in_defs f l <⋆>
binddt (f ⦿ length l) body
    Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall (l : list (term v1)) (body : term v1),
binddt f (letin l body) =
pure (letin (v:=v2)) <⋆> subst_in_defs f l <⋆>
binddt (f ⦿ length l) body
      intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
l: list (term v1)
body: term v1
binddt f (letin l body) =
pure (letin (v:=v2)) <⋆> subst_in_defs f l <⋆>
binddt (f ⦿ length l) body cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
l: list (term v1)
body: term v1
pure (letin (v:=v2)) <⋆>
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) 0 l <⋆> binddt (f ⦿ length l) body =
pure (letin (v:=v2)) <⋆> subst_in_defs f l <⋆>
binddt (f ⦿ length l) body
      do 2 fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
l: list (term v1)
body: term v1
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) 0 l = subst_in_defs f l
      unfold subst_in_defs.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
l: list (term v1)
body: term v1
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) 0 l = binddt f l
      unfold_ops @Mapdt_Binddt_compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
l: list (term v1)
body: term v1
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) 0 l =
mapdt (fun '(w1, t) => binddt (f ⦿ w1) t) l
      unfold_ops @Mapdt_Telescoping_List.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
l: list (term v1)
body: term v1
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) 0 l =
mapdt_telescoping_list
  (fun '(w1, t) => binddt (f ⦿ w1) t) l
      match goal with
      | |- context[(fun '(w1, t) => ?binddt (f ⦿ w1) t)] =>
          replace (fun '(w1, t) => binddt (f ⦿ w1) t) with
          ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ 0)
          by now ext [w t]
      end.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
l: list (term v1)
body: term v1
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) 0 l =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ 0) l
      generalize dependent f; clear f.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
l: list (term v1)
body: term v1
forall f : nat * v1 -> G (term v2),
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) 0 l =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ 0) l
      generalize 0.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
l: list (term v1)
body: term v1
forall (n : nat) (f : nat * v1 -> G (term v2)),
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) n l =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ n) l
      induction l; intros n f.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
body: term v1
n: nat
f: nat * v1 -> G (term v2)
pure [] =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ n) []
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
a: term v1
l: list (term v1)
body: term v1
IHl: forall (n : nat) (f : nat * v1 -> G (term v2)),
(fix F
   (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) n l =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ n) l
n: nat
f: nat * v1 -> G (term v2)
pure cons <⋆> binddt (f ⦿ n) a <⋆>
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (S n) l =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ n) 
  (a :: l)
      -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
body: term v1
n: nat
f: nat * v1 -> G (term v2)
pure [] =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ n) [] cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
body: term v1
n: nat
f: nat * v1 -> G (term v2)
pure [] = pure []
        reflexivity.
      -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
a: term v1
l: list (term v1)
body: term v1
IHl: forall (n : nat) (f : nat * v1 -> G (term v2)),
(fix F
   (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) n l =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ n) l
n: nat
f: nat * v1 -> G (term v2)
pure cons <⋆> binddt (f ⦿ n) a <⋆>
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (S n) l =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ n) (a :: l) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
a: term v1
l: list (term v1)
body: term v1
IHl: forall (n : nat) (f : nat * v1 -> G (term v2)),
(fix F
   (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) n l =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ n) l
n: nat
f: nat * v1 -> G (term v2)
pure cons <⋆> binddt (f ⦿ n) a <⋆>
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (S n) l =
pure cons <⋆> binddt (f ⦿ (n ● 0)) a <⋆>
mapdt_telescoping_list
  (((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ n) ⦿ 1) l
        rewrite preincr_preincr.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
a: term v1
l: list (term v1)
body: term v1
IHl: forall (n : nat) (f : nat * v1 -> G (term v2)),
(fix F
   (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) n l =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ n) l
n: nat
f: nat * v1 -> G (term v2)
pure cons <⋆> binddt (f ⦿ n) a <⋆>
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (S n) l =
pure cons <⋆> binddt (f ⦿ (n ● 0)) a <⋆>
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ (n ● 1)) l
        specialize (IHl (n ● 1) f).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
a: term v1
l: list (term v1)
body: term v1
n: nat
f: nat * v1 -> G (term v2)
IHl: (fix F
   (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (n ● 1) l =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ (n ● 1))
  l
pure cons <⋆> binddt (f ⦿ n) a <⋆>
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (S n) l =
pure cons <⋆> binddt (f ⦿ (n ● 0)) a <⋆>
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ (n ● 1)) l
        rewrite <- IHl.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
a: term v1
l: list (term v1)
body: term v1
n: nat
f: nat * v1 -> G (term v2)
IHl: (fix F
   (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (n ● 1) l =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ (n ● 1))
  l
pure cons <⋆> binddt (f ⦿ n) a <⋆>
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (S n) l =
pure cons <⋆> binddt (f ⦿ (n ● 0)) a <⋆>
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (n ● 1) l
        replace (n ● 0) with (n) by
          (unfold_ops @Monoid_op_plus; lia).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
a: term v1
l: list (term v1)
body: term v1
n: nat
f: nat * v1 -> G (term v2)
IHl: (fix F
   (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (n ● 1) l =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ (n ● 1))
  l
pure cons <⋆> binddt (f ⦿ n) a <⋆>
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (S n) l =
pure cons <⋆> binddt (f ⦿ n) a <⋆>
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (n ● 1) l
        replace (n ● 1) with (S n) by
          (unfold_ops @Monoid_op_plus; lia).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
a: term v1
l: list (term v1)
body: term v1
n: nat
f: nat * v1 -> G (term v2)
IHl: (fix F
   (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (n ● 1) l =
mapdt_telescoping_list
  ((fun '(w1, t) => binddt (f ⦿ w1) t) ⦿ (n ● 1))
  l
pure cons <⋆> binddt (f ⦿ n) a <⋆>
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (S n) l =
pure cons <⋆> binddt (f ⦿ n) a <⋆>
(fix F (acc : nat) (ls : list (term v1)) {struct ls} :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d0 :: drest =>
       pure cons <⋆> binddt (f ⦿ acc) d0 <⋆>
       F (S acc) drest
   end) (S n) l
        reflexivity.
    Qed.

    Lemma binddt_term_rw4: forall (t1 t2: term v1),
        binddt f (app t1 t2) =
          pure (@app v2) <⋆> binddt f t1 <⋆> binddt f t2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall t1 t2 : term v1,
binddt f (app t1 t2) =
pure (app (v:=v2)) <⋆> binddt f t1 <⋆> binddt f t2
    Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall t1 t2 : term v1,
binddt f (app t1 t2) =
pure (app (v:=v2)) <⋆> binddt f t1 <⋆> binddt f t2
      reflexivity.
    Qed.

  End pointful.

  Section pointfree.

    Context
      `{Applicative G2}
        {B C: Type}
          (g : nat * B -> G2 (term C)).

      Lemma binddt_pointfree_letin_defs: forall l,
          binddt g ∘ letin (v:=B) l =
            (precompose (binddt (g ⦿ length l)) ∘ ap G2)
              (pure (letin (v:=C)) <⋆> (subst_in_defs g l)).G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
forall l : list (term B),
binddt g ∘ letin l =
(precompose (binddt (g ⦿ length l)) ∘ ap G2)
  (pure (letin (v:=C)) <⋆> subst_in_defs g l)
      Proof.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
forall l : list (term B),
binddt g ∘ letin l =
(precompose (binddt (g ⦿ length l)) ∘ ap G2)
  (pure (letin (v:=C)) <⋆> subst_in_defs g l)
        intros l.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
l: list (term B)
binddt g ∘ letin l =
(precompose (binddt (g ⦿ length l)) ∘ ap G2)
  (pure (letin (v:=C)) <⋆> subst_in_defs g l)
        ext body.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
l: list (term B)
body: term B
(binddt g ∘ letin l) body =
(precompose (binddt (g ⦿ length l)) ∘ ap G2)
  (pure (letin (v:=C)) <⋆> subst_in_defs g l) body
        unfold precompose, compose.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
l: list (term B)
body: term B
binddt g (letin l body) =
pure (letin (v:=C)) <⋆> subst_in_defs g l <⋆>
binddt (g ⦿ length l) body
        rewrite binddt_term_rw3.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
l: list (term B)
body: term B
pure (letin (v:=C)) <⋆> subst_in_defs g l <⋆>
binddt (g ⦿ length l) body =
pure (letin (v:=C)) <⋆> subst_in_defs g l <⋆>
binddt (g ⦿ length l) body
        reflexivity.
      Qed.

      Lemma binddt_pointfree_letin: forall `(l:list A),
          compose (binddt g) ∘ letin (v:=B) ∘
            mapdt_make (Mapdt_inst := Mapdt_Telescoping_List) l (B := term B) =
            ((compose (precompose (binddt (g ⦿ length l)) ∘ ap G2) ∘
                precompose (subst_in_defs g) ∘
                ap G2 ∘ pure (F := G2)) (letin (v:=C))) ∘
              mapdt_make (Mapdt_inst := Mapdt_Telescoping_List) l (B := term B).G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
forall (A : Type) (l : list A),
compose (binddt g) ∘ letin (v:=B) ∘ mapdt_make l =
(compose (precompose (binddt (g ⦿ length l)) ∘ ap G2)
 ∘ precompose (subst_in_defs g) ∘ ap G2 ∘ pure)
  (letin (v:=C)) ∘ mapdt_make l
      Proof.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
forall (A : Type) (l : list A),
compose (binddt g) ∘ letin (v:=B) ∘ mapdt_make l =
(compose (precompose (binddt (g ⦿ length l)) ∘ ap G2)
 ∘ precompose (subst_in_defs g) ∘ ap G2 ∘ pure)
  (letin (v:=C)) ∘ mapdt_make l
        intros A l.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
l: list A
compose (binddt g) ∘ letin (v:=B) ∘ mapdt_make l =
(compose (precompose (binddt (g ⦿ length l)) ∘ ap G2)
 ∘ precompose (subst_in_defs g) ∘ ap G2 ∘ pure)
  (letin (v:=C)) ∘ mapdt_make l
        ext l' body.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
l: list A
l': Vector (plength l) (term B)
body: term B
(compose (binddt g) ∘ letin (v:=B) ∘ mapdt_make l) l'
  body =
((compose (precompose (binddt (g ⦿ length l)) ∘ ap G2)
  ∘ precompose (subst_in_defs g) ∘ ap G2 ∘ pure)
   (letin (v:=C)) ∘ mapdt_make l) l' body
        unfold precompose, compose.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
l: list A
l': Vector (plength l) (term B)
body: term B
binddt g (letin (mapdt_make l l') body) =
pure (letin (v:=C)) <⋆>
subst_in_defs g (mapdt_make l l') <⋆>
binddt (g ⦿ length l) body
        rewrite binddt_term_rw3.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
l: list A
l': Vector (plength l) (term B)
body: term B
pure (letin (v:=C)) <⋆>
subst_in_defs g (mapdt_make l l') <⋆>
binddt (g ⦿ length (mapdt_make l l')) body =
pure (letin (v:=C)) <⋆>
subst_in_defs g (mapdt_make l l') <⋆>
binddt (g ⦿ length l) body
        do 2 rewrite <- list_plength_length.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
l: list A
l': Vector (plength l) (term B)
body: term B
pure (letin (v:=C)) <⋆>
subst_in_defs g (mapdt_make l l') <⋆>
binddt (g ⦿ plength (mapdt_make l l')) body =
pure (letin (v:=C)) <⋆>
subst_in_defs g (mapdt_make l l') <⋆>
binddt (g ⦿ plength l) body
        unfold mapdt_make.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
l: list A
l': Vector (plength l) (term B)
body: term B
pure (letin (v:=C)) <⋆>
subst_in_defs g (trav_make l l') <⋆>
binddt (g ⦿ plength (trav_make l l')) body =
pure (letin (v:=C)) <⋆>
subst_in_defs g (trav_make l l') <⋆>
binddt (g ⦿ plength l) body
        rewrite <- plength_trav_make.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
l: list A
l': Vector (plength l) (term B)
body: term B
pure (letin (v:=C)) <⋆>
subst_in_defs g (trav_make l l') <⋆>
binddt (g ⦿ plength l) body =
pure (letin (v:=C)) <⋆>
subst_in_defs g (trav_make l l') <⋆>
binddt (g ⦿ plength l) body
        reflexivity.
      Qed.

    End pointfree.

End rewriting.

#[local] Notation "'P'" := pure.
#[local] Notation "'BD'" := binddt.

Ltac simplify_binddt_term :=
  match goal with
  | |- context[BD ?f (tvar ?y)] =>
      ltac_trace "step_BD_tvar";
      rewrite binddt_term_rw1
  | |- context[((binddt ?f) (abs ?body))] =>
      rewrite binddt_term_rw2
  | |- context[((BD ?f) (letin ?l ?body))] =>
      ltac_trace "step_BD_letin";
      rewrite binddt_term_rw3
  | |- context[((BD ?f) (app ?t1 ?t2))] =>
      ltac_trace "step_BD_app";
      rewrite binddt_term_rw4
  end.

Ltac cbn_binddt ::=
  simplify_binddt_term.

Instantiate simplification infrastructure

Theorem dtm1_term:
  forall `{Applicative G} (A B : Type),
  forall f : nat * A -> G (term B),
    binddt f ∘ ret  = f ∘ ret (T := (nat ×)).forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : nat * A -> G (term B)),
BD f ∘ ret = f ∘ ret
Proof.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : nat * A -> G (term B)),
BD f ∘ ret = f ∘ ret
  derive_dtm1.
Qed.

Theorem dtm2_term : forall A : Type,
    binddt (T := term) (U := term)
      (G := fun A => A) (ret (T := term) ∘ extract (W := (nat ×))) = @id (term A).forall A : Type, BD (ret ∘ extract) = id
Proof.forall A : Type, BD (ret ∘ extract) = id
  intros.A: Type
BD (ret ∘ extract) = id derive_dtm2.A: Type
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs -> BD (ret ∘ extract) t = t
IHt: BD (ret ∘ extract) t = t
subst_in_defs (ret ∘ extract) defs = defs
  unfold subst_in_defs.A: Type
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs -> BD (ret ∘ extract) t = t
IHt: BD (ret ∘ extract) t = t
BD (ret ∘ extract) defs = defs
  unfold_ops @Mapdt_Binddt_compose.A: Type
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs -> BD (ret ∘ extract) t = t
IHt: BD (ret ∘ extract) t = t
mapdt (fun '(w1, t) => BD ((ret ∘ extract) ⦿ w1) t)
  defs = defs
  apply mapdt_respectful_id; intros.A: Type
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs -> BD (ret ∘ extract) t = t
IHt: BD (ret ∘ extract) t = t
e: nat
a: term A
H: (e, a) ∈d defs
BD ((ret ∘ extract) ⦿ e) a = a
  do 2 push_preincr_into_fn.A: Type
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs -> BD (ret ∘ extract) t = t
IHt: BD (ret ∘ extract) t = t
e: nat
a: term A
H: (e, a) ∈d defs
BD (ret ∘ extract) a = a
  apply ind_implies_in in H.A: Type
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs -> BD (ret ∘ extract) t = t
IHt: BD (ret ∘ extract) t = t
e: nat
a: term A
H: a ∈ defs
BD (ret ∘ extract) a = a
  auto.
Qed.

#[local] Set Keyed Unification.

Theorem dtm3_term:
  forall `{Applicative G1} `{Applicative G2},
  forall `(g : nat * B -> G2 (term C)) `(f : nat * A -> G1 (term B)),
    map (binddt g) ∘ binddt f = binddt (G := G1 ∘ G2) (g ⋆7 f).forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall (B C : Type) (g : nat * B -> G2 (term C))
  (A : Type) (f : nat * A -> G1 (term B)),
map (BD g) ∘ BD f = BD (g ⋆7 f)
Proof.forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall (B C : Type) (g : nat * B -> G2 (term C))
  (A : Type) (f : nat * A -> G1 (term B)),
map (BD g) ∘ BD f = BD (g ⋆7 f)
  intros.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
f: nat * A -> G1 (term B)
map (BD g) ∘ BD f = BD (g ⋆7 f)
  derive_dtm3.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
P (compose (BD g) ∘ letin (v:=B)) <⋆>
subst_in_defs f defs <⋆> 
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆> subst_in_defs (g ⋆7 f) defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)

  assert (IHdefs':
           map (F := G1) (subst_in_defs g) (subst_in_defs f defs) =
             subst_in_defs (G := G1 ∘ G2) (g ⋆7 f) defs).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P (compose (BD g) ∘ letin (v:=B)) <⋆>
subst_in_defs f defs <⋆> 
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆> subst_in_defs (g ⋆7 f) defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  {G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
    unfold subst_in_defs.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
map (BD g) (BD f defs) = BD (g ⋆7 f) defs
    unfold_ops @Mapdt_Binddt_compose.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
map (mapdt (fun '(w1, t) => BD (g ⦿ w1) t))
  (mapdt (fun '(w1, t) => BD (f ⦿ w1) t) defs) =
mapdt (fun '(w1, t) => BD ((g ⋆7 f) ⦿ w1) t) defs
    compose near defs on left.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
(map (mapdt (fun '(w1, t) => BD (g ⦿ w1) t))
 ∘ mapdt (fun '(w1, t) => BD (f ⦿ w1) t)) defs =
mapdt (fun '(w1, t) => BD ((g ⋆7 f) ⦿ w1) t) defs
    rewrite kdtf_mapdt2.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
mapdt
  ((fun '(w1, t) => BD (g ⦿ w1) t)
   ⋆3 (fun '(w1, t) => BD (f ⦿ w1) t)) defs =
mapdt (fun '(w1, t) => BD ((g ⋆7 f) ⦿ w1) t) defs
    apply (mapdt_respectful (G := G1 ∘ G2) (T := list) _ _ defs).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
forall (e : nat) (a : term A),
(e, a) ∈d defs ->
((fun '(w1, t) => BD (g ⦿ w1) t)
 ⋆3 (fun '(w1, t) => BD (f ⦿ w1) t)) (
  e, a) = BD ((g ⋆7 f) ⦿ e) a
    intros e t' Hin.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
e: nat
t': term A
Hin: (e, t') ∈d defs
((fun '(w1, t) => BD (g ⦿ w1) t)
 ⋆3 (fun '(w1, t) => BD (f ⦿ w1) t)) (
  e, t') = BD ((g ⋆7 f) ⦿ e) t'
    rewrite <- (kc7_preincr g f e).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
e: nat
t': term A
Hin: (e, t') ∈d defs
((fun '(w1, t) => BD (g ⦿ w1) t)
 ⋆3 (fun '(w1, t) => BD (f ⦿ w1) t)) (
  e, t') = BD (g ⦿ e ⋆7 f ⦿ e) t'
    rewrite kc3_spec.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
e: nat
t': term A
Hin: (e, t') ∈d defs
map ((fun '(w1, t) => BD (g ⦿ w1) t) ∘ pair e)
  (BD (f ⦿ e) t') = BD (g ⦿ e ⋆7 f ⦿ e) t'
    apply ind_implies_in in Hin.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
e: nat
t': term A
Hin: t' ∈ defs
map ((fun '(w1, t) => BD (g ⦿ w1) t) ∘ pair e)
  (BD (f ⦿ e) t') = BD (g ⦿ e ⋆7 f ⦿ e) t'
    rewrite <- (IHdefs t' Hin (g ⦿ e) (f ⦿ e)).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
e: nat
t': term A
Hin: t' ∈ defs
map ((fun '(w1, t) => BD (g ⦿ w1) t) ∘ pair e)
  (BD (f ⦿ e) t') = map (BD (g ⦿ e)) (BD (f ⦿ e) t')
    reflexivity.
  }G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P (compose (BD g) ∘ letin (v:=B)) <⋆>
subst_in_defs f defs <⋆> 
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆> subst_in_defs (g ⋆7 f) defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  unfold subst_in_defs at 1.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P (compose (BD g) ∘ letin (v:=B)) <⋆> BD f defs <⋆>
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆> subst_in_defs (g ⋆7 f) defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  unfold_ops @Mapdt_Binddt_compose.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P (compose (BD g) ∘ letin (v:=B)) <⋆>
mapdt (fun '(w1, t) => BD (f ⦿ w1) t) defs <⋆>
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆> subst_in_defs (g ⋆7 f) defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  rewrite (mapdt_repr (E := nat) (T := list) _ _ defs
             (fun '(w1, t0) => BD (f ⦿ w1) t0)).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P (compose (BD g) ∘ letin (v:=B)) <⋆>
map (mapdt_make defs)
  (forwards
     (traverse
        (mkBackwards
         ∘ (fun '(w1, t0) => BD (f ⦿ w1) t0))
        (mapdt_contents defs))) <⋆>
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆> subst_in_defs (g ⋆7 f) defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  dtm3_push_map_right_to_left.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P
  (precompose (mapdt_make defs)
     (compose (BD g) ∘ letin (v:=B))) <⋆>
forwards
  (traverse
     (mkBackwards ∘ (fun '(w1, t0) => BD (f ⦿ w1) t0))
     (mapdt_contents defs)) <⋆> 
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆> subst_in_defs (g ⋆7 f) defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  repeat change (precompose ?f ?g) with (g ∘ f).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P (compose (BD g) ∘ letin (v:=B) ∘ mapdt_make defs) <⋆>
forwards
  (traverse
     (mkBackwards ∘ (fun '(w1, t0) => BD (f ⦿ w1) t0))
     (mapdt_contents defs)) <⋆> 
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆> subst_in_defs (g ⋆7 f) defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  rewrite binddt_pointfree_letin.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P
  ((compose
      (precompose (BD (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (subst_in_defs g) ∘ 
    ap G2 ∘ P) (letin (v:=C)) ∘ 
   mapdt_make defs) <⋆>
forwards
  (traverse
     (mkBackwards ∘ (fun '(w1, t0) => BD (f ⦿ w1) t0))
     (mapdt_contents defs)) <⋆> 
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆> subst_in_defs (g ⋆7 f) defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  change (?g ∘ ?trav_make defs) with (precompose (trav_make defs) g).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P
  (precompose (mapdt_make defs)
     ((compose
         (precompose (BD (g ⦿ length defs)) ∘ ap G2)
       ∘ precompose (subst_in_defs g) ∘ 
       ap G2 ∘ P) (letin (v:=C)))) <⋆>
forwards
  (traverse
     (mkBackwards ∘ (fun '(w1, t0) => BD (f ⦿ w1) t0))
     (mapdt_contents defs)) <⋆> 
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆> subst_in_defs (g ⋆7 f) defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  rewrite <- app_pure_natural.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
map (precompose (mapdt_make defs))
  (P
     ((compose
         (precompose (BD (g ⦿ length defs)) ∘ ap G2)
       ∘ precompose (subst_in_defs g) ∘ 
       ap G2 ∘ P) (letin (v:=C)))) <⋆>
forwards
  (traverse
     (mkBackwards ∘ (fun '(w1, t0) => BD (f ⦿ w1) t0))
     (mapdt_contents defs)) <⋆> 
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆> subst_in_defs (g ⋆7 f) defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  rewrite ap_map.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P
  ((compose
      (precompose (BD (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (subst_in_defs g) ∘ 
    ap G2 ∘ P) (letin (v:=C))) <⋆>
map (mapdt_make defs)
  (forwards
     (traverse
        (mkBackwards
         ∘ (fun '(w1, t0) => BD (f ⦿ w1) t0))
        (mapdt_contents defs))) <⋆>
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆> subst_in_defs (g ⋆7 f) defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  rewrite <- mapdt_repr.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P
  ((compose
      (precompose (BD (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (subst_in_defs g) ∘ 
    ap G2 ∘ P) (letin (v:=C))) <⋆>
mapdt (fun '(w1, t0) => BD (f ⦿ w1) t0) defs <⋆>
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆> subst_in_defs (g ⋆7 f) defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  change (mapdt (A := term A) (B := term B)
            _ defs) with (subst_in_defs f defs).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P
  ((compose
      (precompose (BD (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (subst_in_defs g) ∘ 
    ap G2 ∘ P) (letin (v:=C))) <⋆>
subst_in_defs f defs <⋆> 
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆> subst_in_defs (g ⋆7 f) defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  rewrite <- IHdefs'.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P
  ((compose
      (precompose (BD (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (subst_in_defs g) ∘ 
    ap G2 ∘ P) (letin (v:=C))) <⋆>
subst_in_defs f defs <⋆> 
BD (f ⦿ length defs) t =
P (P (letin (v:=C))) <⋆>
map (subst_in_defs g) (subst_in_defs f defs) <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  dtm3_rhs_one_constructor.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P
  ((compose
      (precompose (BD (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (subst_in_defs g) ∘ 
    ap G2 ∘ P) (letin (v:=C))) <⋆>
subst_in_defs f defs <⋆> 
BD (f ⦿ length defs) t =
P
  (precompose (subst_in_defs g)
     (ap G2 (P (letin (v:=C))))) <⋆>
subst_in_defs f defs <⋆>
map (BD (g ⦿ length defs)) (BD (f ⦿ length defs) t)
  dtm3_rhs_one_constructor.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (BD g) (BD f t) = BD (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': map (subst_in_defs g) (subst_in_defs f defs) =
subst_in_defs (g ⋆7 f) defs
P
  ((compose
      (precompose (BD (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (subst_in_defs g) ∘ 
    ap G2 ∘ P) (letin (v:=C))) <⋆>
subst_in_defs f defs <⋆> 
BD (f ⦿ length defs) t =
P
  (precompose (BD (g ⦿ length defs))
   ∘ (ap G2
      ∘ precompose (subst_in_defs g)
          (ap G2 (P (letin (v:=C)))))) <⋆>
subst_in_defs f defs <⋆> 
BD (f ⦿ length defs) t
  reflexivity.
Qed.

Theorem dtm4_term :
  forall (G1 G2 : Type -> Type) (H1 : Map G1) (H2 : Mult G1)
    (H3 : Pure G1) (H4 : Map G2) (H5 : Mult G2) (H6 : Pure G2)
    (ϕ : forall A : Type, G1 A -> G2 A),
    ApplicativeMorphism G1 G2 ϕ ->
    forall (A B : Type) (f : nat * A -> G1 (term B)),
      ϕ (term B) ∘ binddt f = binddt (ϕ (term B) ∘ f).forall (G1 G2 : Type -> Type) (H1 : Map G1)
  (H2 : Mult G1) (H3 : Pure G1) (H4 : Map G2)
  (H5 : Mult G2) (H6 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : nat * A -> G1 (term B)),
ϕ (term B) ∘ BD f = BD (ϕ (term B) ∘ f)
Proof.forall (G1 G2 : Type -> Type) (H1 : Map G1)
  (H2 : Mult G1) (H3 : Pure G1) (H4 : Map G2)
  (H5 : Mult G2) (H6 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : nat * A -> G1 (term B)),
ϕ (term B) ∘ BD f = BD (ϕ (term B) ∘ f)
  derive_dtm4.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
ϕ (list (term B)) (subst_in_defs f defs) =
subst_in_defs (ϕ (term B) ∘ f) defs
  compose near defs on left.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
(ϕ (list (term B)) ∘ subst_in_defs f) defs =
subst_in_defs (ϕ (term B) ∘ f) defs
  unfold subst_in_defs.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
(ϕ (list (term B)) ∘ BD f) defs =
BD (ϕ (term B) ∘ f) defs
  unfold_ops @Mapdt_Binddt_compose.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
(ϕ (list (term B))
 ∘ mapdt (fun '(w1, t) => BD (f ⦿ w1) t)) defs =
mapdt (fun '(w1, t) => BD ((ϕ (term B) ∘ f) ⦿ w1) t)
  defs
  change ((?g ∘ ?f) ⦿ ?w) with (g ∘ (f ⦿ w)).G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
(ϕ (list (term B))
 ∘ mapdt (fun '(w1, t) => BD (f ⦿ w1) t)) defs =
mapdt (fun '(w1, t) => BD (ϕ (term B) ∘ f ⦿ w1) t)
  defs
  rewrite kdtf_morph.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
mapdt (ϕ (term B) ∘ (fun '(w1, t) => BD (f ⦿ w1) t))
  defs =
mapdt (fun '(w1, t) => BD (ϕ (term B) ∘ f ⦿ w1) t)
  defs
  apply mapdt_respectful;[typeclasses eauto|].G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
forall (e : nat) (a : term A),
(e, a) ∈d defs ->
(ϕ (term B) ∘ (fun '(w1, t) => BD (f ⦿ w1) t)) (e, a) =
BD (ϕ (term B) ∘ f ⦿ e) a
  introv Hin.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
e: nat
a: term A
Hin: (e, a) ∈d defs
(ϕ (term B) ∘ (fun '(w1, t) => BD (f ⦿ w1) t)) (e, a) =
BD (ϕ (term B) ∘ f ⦿ e) a
  unfold compose.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
e: nat
a: term A
Hin: (e, a) ∈d defs
ϕ (term B) (BD (f ⦿ e) a) = BD (ϕ (term B) ○ f ⦿ e) a
  apply ind_implies_in in Hin.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
e: nat
a: term A
Hin: a ∈ defs
ϕ (term B) (BD (f ⦿ e) a) = BD (ϕ (term B) ○ f ⦿ e) a
  apply IHdefs.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (BD f t) = BD (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
e: nat
a: term A
Hin: a ∈ defs
a ∈ defs
  assumption.
Qed.

#[export] Instance DTM_LetIn: DecoratedTraversableMonad nat term.DecoratedTraversableMonad nat term
Proof.DecoratedTraversableMonad nat term
  constructor.Monoid nat
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : nat * A -> G (term B)),
BD f ∘ ret = f ∘ ret
DecoratedTraversableRightPreModule nat term term
  -Monoid nat typeclasses eauto.
  -forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : nat * A -> G (term B)),
BD f ∘ ret = f ∘ ret intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: nat * A -> G (term B)
BD f ∘ ret = f ∘ ret apply dtm1_term.
  -DecoratedTraversableRightPreModule nat term term constructor.forall A : Type, BD (ret ∘ extract) = id
forall (G1 : Type -> Type) 
  (Map_G : Map G1) (Pure_G : Pure G1)
  (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) 
  (Map_G0 : Map G2) (Pure_G0 : Pure G2)
  (Mult_G0 : Mult G2),
Applicative G2 ->
forall (B C : Type) (g : nat * B -> G2 (term C))
  (A : Type) (f : nat * A -> G1 (term B)),
map (BD g) ∘ BD f = BD (g ⋆7 f)
forall (G1 G2 : Type -> Type) 
  (H : Map G1) (H0 : Mult G1) 
  (H1 : Pure G1) (H2 : Map G2) 
  (H3 : Mult G2) (H4 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : nat * A -> G1 (term B)),
ϕ (term B) ∘ BD f = BD (ϕ (term B) ∘ f)
    +forall A : Type, BD (ret ∘ extract) = id apply dtm2_term.
    +forall (G1 : Type -> Type) 
  (Map_G : Map G1) (Pure_G : Pure G1)
  (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) 
  (Map_G0 : Map G2) (Pure_G0 : Pure G2)
  (Mult_G0 : Mult G2),
Applicative G2 ->
forall (B C : Type) (g : nat * B -> G2 (term C))
  (A : Type) (f : nat * A -> G1 (term B)),
map (BD g) ∘ BD f = BD (g ⋆7 f) intros.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
f: nat * A -> G1 (term B)
map (BD g) ∘ BD f = BD (g ⋆7 f) apply dtm3_term.
    +forall (G1 G2 : Type -> Type) 
  (H : Map G1) (H0 : Mult G1) 
  (H1 : Pure G1) (H2 : Map G2) 
  (H3 : Mult G2) (H4 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : nat * A -> G1 (term B)),
ϕ (term B) ∘ BD f = BD (ϕ (term B) ∘ f) apply dtm4_term.
Qed.