Formalizing variadic syntax with Tealeaves

let with letrec 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.

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

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 ls :=
            match ls with
            | nil => pure nil
            | cons d drest =>
                pure cons <⋆> binddt_term (f ⦿ length defs) d <⋆> F drest
            end) 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.

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_List_Full))
    (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, BD 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, BD 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,
BD f (abs t) = P (abs (v:=v2)) <⋆> BD (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,
BD f (abs t) = P (abs (v:=v2)) <⋆> BD (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),
BD f (letin l body) =
P (letin (v:=v2)) <⋆> subst_in_defs f l <⋆>
BD (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),
BD f (letin l body) =
P (letin (v:=v2)) <⋆> subst_in_defs f l <⋆>
BD (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
BD f (letin l body) =
P (letin (v:=v2)) <⋆> subst_in_defs f l <⋆>
BD (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
P (letin (v:=v2)) <⋆>
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ length l) d <⋆> F drest
   end) l <⋆> BD (f ⦿ length l) body =
P (letin (v:=v2)) <⋆> subst_in_defs f l <⋆>
BD (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 (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ length l) d <⋆> F drest
   end) 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 (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ length l) d <⋆> F drest
   end) l = BD 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 (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ length l) d <⋆> F drest
   end) l = mapdt (fun '(w1, t) => BD (f ⦿ w1) t) l
      unfold_ops @Mapdt_List_Full;
        unfold mapdt_list_full.
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 (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ length l) d <⋆> F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ∘ pair (length l))
  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 (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ length l) d <⋆> F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ 0
   ∘ pair (length l)) l
      match goal with
      | |- context[BD (f ⦿ length l)] =>
          replace (BD (f ⦿ length l)) with
          (BD (f ⦿ (length l + 0)%nat))
      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 (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length l + 0)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ 0
   ∘ pair (length l)) l
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
BD (f ⦿ (length l + 0)) = BD (f ⦿ length l)
      2: {
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
BD (f ⦿ (length l + 0)) = BD (f ⦿ length l) 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
f ⦿ (length l + 0) = f ⦿ length l 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
length l + 0 = length l lia. }
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 (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length l + 0)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ 0
   ∘ pair (length l)) 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 (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length l + 0)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ 0
   ∘ pair (length l)) 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 (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (length l)) 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)
P [] =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (length [])) []
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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (length l)) l
n: nat
f: nat * v1 -> G (term v2)
P cons <⋆> BD (f ⦿ (length (a :: l) + n)) a <⋆>
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length (a :: l) + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (length (a :: l))) 
  (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)
P [] =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (length [])) [] 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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (length l)) l
n: nat
f: nat * v1 -> G (term v2)
P cons <⋆> BD (f ⦿ (length (a :: l) + n)) a <⋆>
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length (a :: l) + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (length (a :: l))) (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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (length l)) l
n: nat
f: nat * v1 -> G (term v2)
P cons <⋆> BD (f ⦿ S (length l + n)) a <⋆>
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ S (length l + n)) d <⋆>
       F drest
   end) l =
P cons <⋆> BD (f ⦿ (n ● S (length l))) a <⋆>
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (S (length l))) l
        fequal.
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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (length l)) l
n: nat
f: nat * v1 -> G (term v2)
P cons <⋆> BD (f ⦿ S (length l + n)) a =
P cons <⋆> BD (f ⦿ (n ● S (length l))) a
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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (length l)) l
n: nat
f: nat * v1 -> G (term v2)
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ S (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (S (length l))) l
        +
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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (length l)) l
n: nat
f: nat * v1 -> G (term v2)
P cons <⋆> BD (f ⦿ S (length l + n)) a =
P cons <⋆> BD (f ⦿ (n ● S (length l))) a repeat fequal.
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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (length l)) l
n: nat
f: nat * v1 -> G (term v2)
S (length l + n) = n ● S (length l)
          unfold_all_transparent_tcs.
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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (length l)) l
n: nat
f: nat * v1 -> G (term v2)
S (length l + n) = n + S (length l)
          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
IHl: forall (n : nat) (f : nat * v1 -> G (term v2)),
(fix F (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (length l)) l
n: nat
f: nat * v1 -> G (term v2)
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ S (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (S (length l))) l specialize (IHl (S n) 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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ (length l + S n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ S n
   ∘ pair (length l)) l
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ S (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (S (length l))) l
          replace (length l + S n)
            with (S (length l + n)) in IHl by 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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ S (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ S n
   ∘ pair (length l)) l
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ S (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (S (length l))) 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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ S (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ S n
   ∘ pair (length l)) l
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ S n
   ∘ pair (length l)) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
   ∘ pair (S (length l))) l
          fequal.
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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ S (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ S n
   ∘ pair (length l)) l
(fun '(w1, t) => BD (f ⦿ w1) t) ⦿ S n
∘ pair (length l) =
(fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
∘ pair (S (length l))
          ext t.
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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ S (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ S n
   ∘ pair (length l)) l
t: term v1
((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ S n
 ∘ pair (length l)) t =
((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ n
 ∘ pair (S (length l))) t
          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
n: nat
f: nat * v1 -> G (term v2)
IHl: (fix F (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ S (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ S n
   ∘ pair (length l)) l
t: term v1
BD (f ⦿ S (n ● length l)) t =
BD (f ⦿ (n ● S (length l))) t fequal.
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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ S (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ S n
   ∘ pair (length l)) l
t: term v1
f ⦿ S (n ● length l) = f ⦿ (n ● S (length l)) fequal.
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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ S (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ S n
   ∘ pair (length l)) l
t: term v1
S (n ● length l) = n ● S (length l)
          unfold_all_transparent_tcs.
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 (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => P []
   | d :: drest =>
       P cons <⋆> BD (f ⦿ S (length l + n)) d <⋆>
       F drest
   end) l =
traverse
  ((fun '(w1, t) => BD (f ⦿ w1) t) ⦿ S n
   ∘ pair (length l)) l
t: term v1
S (n + length l) = n + S (length l)
          lia.
    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,
BD f (app t1 t2) =
P (app (v:=v2)) <⋆> BD f t1 <⋆> BD 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,
BD f (app t1 t2) =
P (app (v:=v2)) <⋆> BD f t1 <⋆> BD 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),
BD g ∘ letin l =
(precompose (BD (g ⦿ length l)) ∘ ap G2)
  (P (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),
BD g ∘ letin l =
(precompose (BD (g ⦿ length l)) ∘ ap G2)
  (P (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)
BD g ∘ letin l =
(precompose (BD (g ⦿ length l)) ∘ ap G2)
  (P (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
(BD g ∘ letin l) body =
(precompose (BD (g ⦿ length l)) ∘ ap G2)
  (P (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
BD g (letin l body) =
P (letin (v:=C)) <⋆> subst_in_defs g l <⋆>
BD (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
P (letin (v:=C)) <⋆> subst_in_defs g l <⋆>
BD (g ⦿ length l) body =
P (letin (v:=C)) <⋆> subst_in_defs g l <⋆>
BD (g ⦿ length l) body
        reflexivity.
      Qed.

      Lemma binddt_pointfree_letin: forall `(l:list A),
          compose (binddt g) ∘ letin (v:=B) ∘ mapdt_make 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 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 (BD g) ∘ letin (v:=B) ∘ mapdt_make l =
(compose (precompose (BD (g ⦿ length l)) ∘ ap G2)
 ∘ precompose (subst_in_defs g) ∘ ap G2 ∘ P)
  (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 (BD g) ∘ letin (v:=B) ∘ mapdt_make l =
(compose (precompose (BD (g ⦿ length l)) ∘ ap G2)
 ∘ precompose (subst_in_defs g) ∘ ap G2 ∘ P)
  (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 (BD g) ∘ letin (v:=B) ∘ mapdt_make l =
(compose (precompose (BD (g ⦿ length l)) ∘ ap G2)
 ∘ precompose (subst_in_defs g) ∘ ap G2 ∘ P)
  (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 (BD g) ∘ letin (v:=B) ∘ mapdt_make l) l' body =
((compose (precompose (BD (g ⦿ length l)) ∘ ap G2)
  ∘ precompose (subst_in_defs g) ∘ ap G2 ∘ P)
   (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
BD g (letin (mapdt_make l l') body) =
P (letin (v:=C)) <⋆> subst_in_defs g (mapdt_make l l') <⋆>
BD (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
P (letin (v:=C)) <⋆> subst_in_defs g (mapdt_make l l') <⋆>
BD (g ⦿ length (mapdt_make l l')) body =
P (letin (v:=C)) <⋆> subst_in_defs g (mapdt_make l l') <⋆>
BD (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
P (letin (v:=C)) <⋆> subst_in_defs g (mapdt_make l l') <⋆>
BD (g ⦿ plength (mapdt_make l l')) body =
P (letin (v:=C)) <⋆> subst_in_defs g (mapdt_make l l') <⋆>
BD (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
P (letin (v:=C)) <⋆> subst_in_defs g (trav_make l l') <⋆>
BD (g ⦿ plength (trav_make l l')) body =
P (letin (v:=C)) <⋆> subst_in_defs g (trav_make l l') <⋆>
BD (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
P (letin (v:=C)) <⋆> subst_in_defs g (trav_make l l') <⋆>
BD (g ⦿ plength l) body =
P (letin (v:=C)) <⋆> subst_in_defs g (trav_make l l') <⋆>
BD (g ⦿ plength l) body
        reflexivity.
      Qed.

    End pointfree.

  End rewriting.

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.

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.

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 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 ⋆7 f) ⦿ e) t'
    setoid_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
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 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)) <⋆>
map (mapdt_make defs)
  (forwards
     (traverse
        (mkBackwards ∘ (fun '(w1, t) => BD (f ⦿ w1) t))
        (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, t) => BD (f ⦿ w1) t))
     (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, t) => BD (f ⦿ w1) t))
     (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, t) => BD (f ⦿ w1) t))
     (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, t) => BD (f ⦿ w1) t))
     (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, t) => BD (f ⦿ w1) t))
     (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, t) => BD (f ⦿ w1) t))
        (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, 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)
  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.