Fixpoint directly_box containee container :=
  match container with
  | Top | Var _ | Zero => False
  | And s t
  | App s t => directly_box containee s \/ directly_box containee t
  | TLam s
  | TAll s
  | Neu s
  | Imp s _
  | Lam s _
  | TApp s _ => directly_box containee s
  | Box s => s = containee
  end.

(* The predicate db u s n states that u is directly_boxed in s and
   below n recipe binders. *)
(*?*) Inductive db : recipe -> recipe -> nat -> Prop :=
(*?*) | db_box u s : u = s -> db u (Box s) 0
(*?*) | db_lam u s U n : db u s n -> db u (Lam s U) n.+1
(*?*) | db_andl u s t n : db u s n -> db u (And s t) n
(*?*) | db_andr u s t n : db u t n -> db u (And s t) n
(*?*) | db_appl u s t n : db u s n -> db u (App s t) n
(*?*) | db_appr u s t n : db u t n -> db u (App s t) n
(*?*) | db_tlam u s n : db u s n -> db u (TLam s) n
(*?*) | db_tall u s n : db u s n -> db u (TAll s) n
(*?*) | db_imp u s f n : db u s n -> db u (Imp s f) n
(*?*) | db_neu u s n : db u s n -> db u (Neu s) n
(*?*) | db_tapp u s T n : db u s n -> db u (TApp s T) n.
(*?*)
(*?*) Lemma directly_box_db_coincide u s :
(*?*) directly_box u s <-> exists n, db u s n.
(*?*) Proof.
(*?*) elim: s u =>/=.
(*?*) - by move=> *; split=>//; move=> [n h]; inv h.
(*?*) - by move=> *; split=>//; move=> [n h]; inv h.
(*?*) - by move=> *; split=>//; move=> [n h]; inv h.
(*?*) - move=> s h1 t h2 u; split.
(*?*) + move=> [hs|ht].
(*?*) by have[n hn]:= (proj1 (h1 u) hs); exists n; constructor.
(*?*) by have[n hn]:= (proj1 (h2 u) ht); exists n; constructor.
(*?*) + move=> [n hn]. inv hn.
(*?*) by left; apply h1; exists n.
(*?*) by right; apply h2; exists n.
(*?*) - move=> s h1 t h2 u; split.
(*?*) + move=> [hs|ht].
(*?*) by have[n hn]:= (proj1 (h1 u) hs); exists n; constructor.
(*?*) by have[n hn]:= (proj1 (h2 u) ht); exists n; constructor.
(*?*) + move=> [n hn]. inv hn.
(*?*) by left; apply h1; exists n.
(*?*) by right; apply h2; exists n.
(*?*) - move=> s h1 T u; split.
(*?*) + move=> h.
(*?*) by have[n hn]:= (proj1 (h1 u) h); exists n; constructor.
(*?*) + move=> [n hn]. inv hn.
(*?*) by apply h1; exists n.
(*?*) - move=> s h1 U u; split.
(*?*) + move=> h.
(*?*) by have[n hn]:= (proj1 (h1 u) h); exists n.+1; constructor.
(*?*) + move=> [m hn]. inv hn.
(*?*) by apply h1; exists n.
(*?*) - move=> s h1 ? u; split.
(*?*) + move=> h.
(*?*) by have[n hn]:= (proj1 (h1 u) h); exists n; constructor.
(*?*) + move=> [n hn]. inv hn.
(*?*) by apply h1; exists n.
(*?*) - move=> s h1 u; split.
(*?*) + move=> h.
(*?*) by have[n hn]:= (proj1 (h1 u) h); exists n; constructor.
(*?*) + move=> [n hn]. inv hn.
(*?*) by apply h1; exists n.
(*?*) - move=> s h1 u; split.
(*?*) + move=> h.
(*?*) by have[n hn]:= (proj1 (h1 u) h); exists n; constructor.
(*?*) + move=> [n hn]. inv hn.
(*?*) by apply h1; exists n.
(*?*) - move=> s h1 u; split=> [e|[n hn]].
(*?*) + apply h1 in e as [n hn]. exists n. by constructor.
(*?*) + inv hn. apply h1. by exists n.
(*?*) - move=> s h1 u; split=> [e|[n hn]]//.
(*?*) + eexists. by constructor.
(*?*) + by inv hn.
(*?*) Qed.

Definition ctx_ext (Γ Δ: ctx) :=
  exists len, forall i, Γ (i + len) = Δ i.

Lemma ctx_ext0 Γ :
  ctx_ext Γ Γ.
Proof.
  exists 0=> i.
  by rewrite addn0.
Qed.

Lemma ctx_ext1 Δ U Γ :
  ctx_ext Δ (U .: Γ) ->
  ctx_ext Δ Γ.
Proof.
  move=> [len h].
  exists len.+1=> x.
  by rewrite -addSnnS h.
Qed.

Lemma directly_box_ty_ext r s Γ U a b :
  [ Γ, a, b ⊢ r :- U ] ->
  directly_box s r ->
  exists Δ V c, [ Δ, 0, c ⊢ s :- V ] /\ ctx_ext Δ Γ.
Proof.
  move=> h.
  elim: h s=>{r Γ U a b}; try by move=> //=.
  - by move=> > ????? [] h; eauto.
  - by move=> > ????? [] h; eauto.
  - move=> ??????? h3 ? /= h4.
    have{h3 h4}[D [U [c [? h]]]]:= (h3 _ h4).
    exists D, U, c; split=>//.
    by apply ctx_ext1 in h.
  - move=> Γ a b u U hc hty ih t /= <-.
    exists Γ, U, b. split=>//.
    exact: ctx_ext0.
Qed.

Lemma directly_box_dec ee er : decidable (directly_box ee er).
Proof.
  elim: er=>//=; try (by left); try (by right).
  - move=> > [] ? > [] ?;
    try by (left; tauto);
    try by (right; tauto).
    right.
    by case; eauto.
  - move=> > [] ? > [] ?;
    try by (left; tauto);
    try by (right; tauto).
    right.
    by case; eauto.
  - move=> *. exact: recipe_eq_dec.
Qed.

Lemma directly_box_ty r s U Γ a b :
  [ Γ, a, b ⊢ r :- U ] ->
  directly_box s r ->
  closed s ->
  exists V, [ ⊢ s :- V ].
Proof.
  elim: r s U Γ a b =>//.
  - by move=> > ? > ? > hty /= []*; inv hty; eauto.
  - by move=> > ? > ? > hty /= []*; inv hty; eauto.
  - by move=> > ? > hty /= *; inv hty; eauto.
  - by move=> > ? > hty /= *; inv hty; eauto.
  - by move=> > ? > hty /= *; inv hty; eauto.
  - by move=> > ? > hty /= *; inv hty; eauto.
  - by move=> > ? > hty /= *; inv hty; eauto.
  - by move=> > ? > hty /= *; inv hty; eauto.
  - move=> s hs u U Γ a b hty /= <- hc.
    exists U. inv hty.
    apply (has_type_lower_b (b:=b))=>//.
    by apply closed_has_ty_contr with Γ.
Qed.

Lemma directly_box_depth n s r :
  depth r <= n.+1 ->
  directly_box s r ->
  depth s <= n.
Proof.
  elim: r s n; try by move=>//=.
  - move=> s hs t ht ? n /= ? [] *.
    + have h: depth s <= n.+1 by lia.
      exact: (hs _ _ h).
    + have h: depth t <= n.+1 by lia.
      exact: (ht _ _ h).
  - move=> s hs t ht ? n /= ? [] *.
    + have h: depth s <= n.+1 by lia.
      by apply (hs _ _ h).
    + have h: depth t <= n.+1 by lia.
      exact: (ht _ _ h).
  - move=> ???? /= ? <-.
    by lia.
Qed.

Fixpoint subterm sub r :=
  sub = r \/
  match r with
  | Top | Var _ | Zero => False
  | And s t
  | App s t => subterm sub s \/ subterm sub t
  | TLam s
  | TAll s
  | Neu s
  | Imp s _
  | Lam s _
  | Box s
  | TApp s _ => subterm sub s
  end.

Lemma subterm_refl s :
  subterm s s.
Proof.
  by case: s=>/=; by left.
Qed.

Lemma subterm_directly_box s t :
  directly_box s t ->
  subterm s t.
Proof.
  elim: t=>//=; try by auto.
  - by move=> u hu t ht []?; auto.
  - by move=> u hu t ht []?; auto.
  - move=> u hu e. subst. right. by apply subterm_refl.
Qed.

Lemma subterm_neu_idempotent s r :
  subterm s (neu r) ->
  s = neu s.
Proof.
  elim: r=>//=.
  - move=> > []? //. by subst.
  - move=> []? //. by subst.
  - move=> []? //. by subst.
  - move=> u hu t ht [|[]]?; [|by auto|by auto].
    subst=>/=. by rewrite !neu_idempotent.
  - move=> u hu t ht [|[]]?; [|by auto|by auto].
    subst=>/=. by rewrite !neu_idempotent.
  - move=> u hu S []?; [|by auto].
    subst=>/=. by rewrite !neu_idempotent.
  - move=> u hu S []?; [|by auto].
    subst=>/=. by rewrite !neu_idempotent.
  - move=> u hu S []?; [|by auto].
    subst=>/=. by rewrite !neu_idempotent.
  - move=> u hu []?; [|by auto].
    subst=>/=. by rewrite !neu_idempotent.
  - move=> u hu []?; [|by auto].
    subst=>/=. by rewrite !neu_idempotent.
  - move=> u hu []?; [|by auto].
    subst=>/=. by rewrite !neu_idempotent.
  - move=> u hu []?; [|by auto].
    subst=>/=. by rewrite !neu_idempotent.
Qed.

Corollary directly_box_neu_idempotent s r :
  directly_box s (neu r) ->
  s = neu s.
Proof.
  move/subterm_directly_box.
  by apply subterm_neu_idempotent.
Qed.

Lemma directly_box_neu s t :
  directly_box s t ->
  directly_box (neu s) (neu t).
Proof.
  elim: t s=>//=.
  - by move=> s h1 t h2 u []h; [left|right]; auto.
  - by move=> s h1 t h2 u []h; [left|right]; auto.
  - by move=> s h1 u ->.
Qed.

Fixpoint mem_box r :=
  match r with
  | Top | Var _ | Zero => False
  | And s t
  | App s t => mem_box s \/ mem_box t
  | TLam s
  | TAll s
  | Neu s
  | Imp s _
  | Lam s _
  | TApp s _ => mem_box s
  | Box _ => True
  end.

Lemma directly_box_mem_box r :
  forall s, directly_box s r -> mem_box r.
Proof.
  elim: r=>//=.
  - move=> > hs > ht r [] *.
    by left; exact: (hs r).
    by right; exact: (ht r).
  - move=> > hs > ht r [] *.
    by left; exact: (hs r).
    by right; exact: (ht r).
Qed.

Lemma mem_box_depth r :
  depth r = 0 -> not (mem_box r).
Proof.
  elim: r=>//=; try by tauto.
  - move=> > hs > ht ? [] *.
    apply hs; by [|lia].
    apply ht; by [|lia].
  - move=> > hs > ht ? [] *.
    apply hs; by [|lia].
    apply ht; by [|lia].
Qed.

Lemma directly_box_closed s r U Γ a b :
  directly_box s r ->
  [ Γ, a, b ⊢ r :- U ] ->
  closed s.
Proof.
  elim: r s U Γ a b;
  try (by move=> > h; inv h).
  - by move=> ???? > /= [hl|hr] ht; inv ht; eauto.
  - by move=> ???? > /= [hl|hr] ht; inv ht; eauto.
  - by move=> ?? > /= h0 ht; inv ht; eauto.
  - by move=> ?? > /= h0 ht; inv ht; eauto.
  - by move=> ?? > /= h0 ht; inv ht; eauto.
  - by move=> ?? > /= h0 ht; inv ht; eauto.
  - by move=> ?? > /= h0 ht; inv ht; eauto.
  - by move=> ?? > /= h0 ht; inv ht; eauto.
  - by move=> ?? > /= h0 ht; inv ht; eauto.
Qed.

Inductive db3 : recipe -> recipe -> recipe -> recipe -> recipe -> recipe -> Prop :=
| db_box3 u v w r s t : u = r -> v = s -> w = t -> db3 u v w (Box r) (Box s) (Box t)
| db_lam3 u v w r s t U :
    db3 u v w r s t -> db3 u v w (Lam r U) (Lam s U) (Lam t U)
| db_andl3 u v w r1 r2 s1 s2 t1 t2 :
    db3 u v w r1 s1 t1 ->
    db3 u v w (And r1 r2) (And s1 s2) (And t1 t2)
| db_andr3 u v w r1 r2 s1 s2 t1 t2 :
    db3 u v w r2 s2 t2 ->
    db3 u v w (And r1 r2) (And s1 s2) (And t1 t2)
| db_appl3 u v w r1 r2 s1 s2 t1 t2 :
    db3 u v w r1 s1 t1 ->
    db3 u v w (App r1 r2) (App s1 s2) (App t1 t2)
| db_appr3 u v w r1 r2 s1 s2 t1 t2 :
    db3 u v w r2 s2 t2 ->
    db3 u v w (App r1 r2) (App s1 s2) (App t1 t2)
| db_tlam3 u v w r s t :
    db3 u v w r s t -> db3 u v w (TLam r) (TLam s) (TLam t)
| db_tall3 u v w r s t :
    db3 u v w r s t -> db3 u v w (TAll r) (TAll s) (TAll t)
| db_imp3 u v w r s t f :
    db3 u v w r s t -> db3 u v w (Imp r f) (Imp s f) (Imp t f)
| db_neu3 u v w r s t :
    db3 u v w r s t -> db3 u v w (Neu r) (Neu s) (Neu t)
| db_tapp3 u v w r s t T :
    db3 u v w r s t ->
    db3 u v w (TApp r T) (TApp s T) (TApp t T).

Lemma db3_proj1 u v w r s t :
  db3 u v w r s t ->
  directly_box u r.
Proof.
  elim: r s t;
    by first
     [ move=> > h; inv h
     | move=> ?????? /= h; inv h; [left|right]; eauto
     | move=> ????? /= h; inv h; eauto
     | move=> ???? /= h; inv h; eauto ].
Qed.

Lemma db3_proj2 u v w r s t :
  db3 u v w r s t ->
  directly_box v s.
Proof.
  elim: s r t;
    by first
     [ move=> > h; inv h
     | move=> ?????? /= h; inv h; [left|right]; eauto
     | move=> ????? /= h; inv h; eauto
     | move=> ???? /= h; inv h; eauto ].
Qed.

Lemma db3_proj3 u v w r s t :
  db3 u v w r s t ->
  directly_box w t.
Proof.
  elim: t r s;
    by first
     [ move=> > h; inv h
     | move=> ?????? /= h; inv h; [left|right]; eauto
     | move=> ????? /= h; inv h; eauto
     | move=> ???? /= h; inv h; eauto ].
Qed.