Ltac ty_beta_tac U :=
  apply has_type_beta_gen with U=>//;
  first [ apply closed_box
        | apply closedh_box
        | constructor ].

Inductive box_rel P : recipe -> Prop :=
  | box_rel_box s U :
      closed s ->
      [ ⊢ s :- U ] ->
      (forall ξ, strongly (logrel P U) s.|[ren ξ]) ->
      box_rel P (Box s)
  | box_rel_tlam s : box_rel P s -> box_rel P (TLam s)
  | box_rel_tall s : box_rel P s -> box_rel P (TAll s)
  | box_rel_neu s : box_rel P s -> box_rel P (Neu s)
  | box_rel_imp s f : box_rel P s -> box_rel P (Imp s f)
  | box_rel_lam s U : box_rel P s -> box_rel P (Lam s U)
  | box_rel_tapp s T : box_rel P s -> box_rel P (TApp s T)
  | box_rel_var x : box_rel P (Var x)
  | box_rel_top : box_rel P Top
  | box_rel_zero : box_rel P Zero
  | box_rel_app s t : box_rel P s -> box_rel P t -> box_rel P (App s t)
  | box_rel_and s t : box_rel P s -> box_rel P t -> box_rel P (And s t).

Lemma box_rel_preserved_subst P :
  forall s n U t,
  closed t ->
  [ ⊢ t :- U ] ->
  (forall ξ, strongly (logrel P U) t.|[ren ξ]) ->
  box_rel P s ->
  box_rel P s.[Box t//n].
Proof.
  elim=>//=.
  - move=> x n U t hc ht hst _.
    rewrite /subst_var.
    (* the box is created here *)
    case (lt_eq_lt_dec x n)=> [[]|] hn; try by apply box_rel_var.
    by apply box_rel_box with U.
  (* Zero and Top are discharged by the // of elim *)
  - move=> > hs > ht > ??? hb.
    inv hb.
    by constructor; eauto.
  - move=> > hs > ht > ??? hb.
    inv hb.
    by constructor; eauto.
  - move=> > hs > ??? hb.
    inv hb.
    by constructor; eauto.
  - move=> s hs W n U u ??? hb.
    inv hb.
    rewrite upn1 subst_var_lemma.
    have->: (Box u).[ren (+1)] = Box u by apply closed_subst, closed_box.
    by constructor; eauto.
  - move=> > hs > ??? hb.
    inv hb.
    by constructor; eauto.
  - move=> s hs n U u hcu htu hsu hb.
    inv hb.
    (* the box travels under the binder, so its content is shifted *)
    rewrite subst_var_hsubst /=.
    constructor; apply hs with U=> [||θ|]; last by [].
    + by apply closed_unaffectedh.
    + by apply has_type_hsubst_0.
    + by asimpl; apply hsu.
  - move=> s hs n U u hcu htu hsu hb.
    inv hb.
    rewrite subst_var_hsubst /=.
    constructor; apply hs with U=> [||θ|]; last by [].
    + by apply closed_unaffectedh.
    + by apply has_type_hsubst_0.
    + by asimpl; apply hsu.
  - move=> > hs > ??? hb.
    inv hb.
    by constructor; eauto.
  - move=> s hs n U u ??? hb.
    inv hb.
    (* the substitution does not enter a box: its content is closed *)
    rewrite closed_subst=>//.
    by apply box_rel_box with U0.
Qed.

Corollary box_rel_preserved_subst0 P s U t :
  closed t ->
  [ ⊢ t :- U ] ->
  (forall ξ, strongly (logrel P U) t.|[ren ξ]) ->
  box_rel P s ->
  box_rel P s.[Box t/].
Proof.
  move=> *.
  have:= @box_rel_preserved_subst P s 0 U t.
  rewrite -subst_var_0.
  by apply.
Qed.

Lemma up_ren_term (ζ : var -> var) :
  (up (ren ζ) : var -> term) = ren (upren ζ).
Proof. f_ext. by case=> [|y]; asimpl. Qed.

Lemma box_rel_preserved_ren P s ξ :
  box_rel P s ->
  box_rel P s.|[ren ξ].
Proof.
  elim: s ξ
    => [x|||s hs t ht|s hs t ht|s hs S|s hs W|s hs f|s hs|s hs|s hs|s hs] ξ hb /=;
    try (by constructor);
    try (by inv hb; constructor; eauto).
  - by rewrite up_ren_term; inv hb; apply box_rel_tlam; apply hs.
  - by rewrite up_ren_term; inv hb; apply box_rel_tall; apply hs.
  - inv hb.
    apply box_rel_box with U=> [||ξ'].
    + by apply closed_unaffectedh.
    + by apply has_type_hsubst_0.
    + by asimpl.
Qed.

Lemma box_rel_preserved_hsubst P r Γ U a b d T :
  d < b ->
  [ Γ, a, b ⊢ r :- U ] ->
  box_rel P r ->
  box_rel P r.|[upn d (T .: ids)].
Proof.
  elim: r Γ U a b d=>/=.
  - by move=> *; apply box_rel_var.
  - by move=> *; apply box_rel_zero.
  - by move=> *; apply box_rel_top.
  - move=> s h1 t h2 Γ U a b d hdb hty hb; inv hty; inv hb.
    by apply box_rel_and; [apply h1 with Γ U a b|apply h2 with Γ U a b].
  - move=> s h1 t h2 Γ U a b d hdb hty hb; inv hty; inv hb.
    by apply box_rel_app; [apply h1 with Γ (Arr U0 U) a b|apply h2 with Γ U0 a b].
  - move=> s h1 S Γ U a b d hdb hty hb; inv hty; inv hb.
    by apply box_rel_tapp; apply h1 with Γ (TArr U) a b.
  - move=> s h1 W Γ U a b d hdb hty hb; inv hty; inv hb.
    by apply box_rel_lam; apply h1 with (W .: Γ) V a b.
  - move=> s h1 f Γ U a b d hdb hty hb; inv hty; inv hb.
    by apply box_rel_imp; apply h1 with Γ Void a b.
  - move=> s h1 Γ U a b d hdb hty hb; inv hty; inv hb.
    rewrite fold_up_upn.
    by apply box_rel_tlam; apply h1 with Γ U0 a.+1 b.+1; [lia| |].
  - move=> s h1 Γ U a b d hdb hty hb; inv hty; inv hb.
    rewrite fold_up_upn.
    by apply box_rel_tall; apply h1 with Γ Void a.+1 b.+1; [lia| |].
  - move=> s h1 Γ U a b d hdb hty hb; inv hty; inv hb.
    by apply box_rel_neu; apply h1 with Γ U a b.
  - move=> s h1 Γ U a b d hdb hty hb; inv hty; inv hb.
    rewrite (hsubst_T_is_ren (Γ:=Γ) (U:=U) (a:=0) (b:=b))=>//.
    apply box_rel_box with U0=> [||ξ'].
    + by apply closed_unaffectedh.
    + by apply has_type_hsubst_0.
    + by asimpl.
Qed.

Corollary box_rel_preserved_hsubst0 P r Γ U a b T :
  1 <= b ->
  [ Γ, a, b ⊢ r :- U ] ->
  box_rel P r ->
  box_rel P r.|[T/].
Proof.
  move=> hb hty h.
  have:= @box_rel_preserved_hsubst P r Γ U a b 0 T.
  rewrite upn0. by apply.
Qed.

Lemma box_rel_preserved_neu P s :
  box_rel P s ->
  box_rel P (neu s).
Proof.
  elim=>{s}//=; try by constructor.
  move=> s U hc ht h.
  apply box_rel_box with U.
  - by apply closed_sneu.
  - by apply has_type_neu.
  - move=> θ; rewrite -neu_hsubst_comm.
    have[??]:= h θ.
    by split; rewrite ?neu_idempotent.
Qed.

Lemma unfold_box_rel P r Γ U a b :
  [ Γ, a, b ⊢ r :- U ] ->
  (forall s V, directly_box s r -> [ ⊢ s :- V ] ->
     forall ξ, strongly (logrel P V) s.|[ren ξ]) ->
  box_rel P r.
Proof.
  elim: r Γ U a b.
  - by move=> *; constructor.
  - by move=> *; constructor.
  - by move=> *; constructor.
  - move=> s hs t ht Γ U a b hty ih.
    constructor.
    + apply hs with Γ U a b; first by inv hty.
      move=> > hdb. apply: ih. by left.
    + apply ht with Γ U a b; first by inv hty.
      move=> > hdb. apply: ih. by right.
  - move=> s hs t ht Γ U a b hty ih.
    have[W [hs1 ht1]]:
      exists W, [ Γ, a, b ⊢ s :- Arr W U ] /\ [ Γ, a, b ⊢ t :- W ]
      by inv hty; eauto.
    constructor.
    + apply hs with Γ (Arr W U) a b; first by [].
      move=> > hdb. apply: ih. by left.
    + apply ht with Γ W a b; first by [].
      move=> > hdb. apply: ih. by right.
  - move=> s hs T Γ U a b hty ih.
    constructor.
    apply hs with Γ (TArr U) a b; first by inv hty.
    by move=> > hdb; apply: ih.
  - move=> s hs W Γ U a b hty ih.
    have[V hs1]: exists V, [ W .: Γ, a, b ⊢ s :- V ] by inv hty; eauto.
    constructor.
    apply hs with (W .: Γ) V a b; first by [].
    by move=> > hdb; apply: ih.
  - move=> s hs f Γ U a b hty ih.
    constructor.
    apply hs with Γ U a b; first by inv hty.
    by move=> > hdb; apply: ih.
  - move=> s hs Γ U a b hty ih.
    have[V hs1]: exists V, [ Γ, a.+1, b.+1 ⊢ s :- V ] by inv hty; eauto.
    constructor.
    apply hs with Γ V a.+1 b.+1; first by [].
    by move=> > hdb; apply: ih.
  - move=> s hs Γ U a b hty ih.
    constructor.
    apply hs with Γ U a.+1 b.+1; first by inv hty.
    by move=> > hdb; apply: ih.
  - move=> s hs Γ U a b hty ih.
    constructor.
    apply hs with Γ U a b; first by inv hty.
    by move=> > hdb; apply: ih.
  - move=> s hs Γ U a b hty ih.
    inv hty.
    have hts: [ ⊢ s :- U ].
    { apply (has_type_lower_b (b:=b))=>//.
      by apply closed_has_ty_contr with Γ. }
    have?: forall ξ, strongly (logrel P U) s.|[ren ξ] by apply ih.
    by apply box_rel_box with U.
Qed.

Lemma box_rel_box_ids P s :
  box_rel P (Box s) ->
  exists U, closed s /\ [ ⊢ s :- U ] /\ strongly (logrel P U) s.
Proof.
  move=> h; inv h.
  exists U; split=>//; split=>//.
  have hh: strongly (logrel P U) s.|[ids] by apply H2.
  by asimpl in hh.
Qed.

Lemma box_rel_nobox P s :
  ~ mem_box s -> box_rel P s.
Proof.
  elim: s
    => [x|||s hs t ht|s hs t ht|s hs S|s hs W|s hs f|s hs|s hs|s hs|s hs] /= h;
    try by constructor.
  - constructor; by [apply hs=> ?; apply h; left | apply ht=> ?; apply h; right].
  - constructor; by [apply hs=> ?; apply h; left | apply ht=> ?; apply h; right].
  - by constructor; apply hs.
  - by constructor; apply hs.
  - by constructor; apply hs.
  - by constructor; apply hs.
  - by constructor; apply hs.
  - by constructor; apply hs.
  - by exfalso; apply h.
Qed.

(* Relation R strongly holds on the recipes bellow boxes .... TODO *)

Inductive box_rel2 P : recipe -> recipe -> Prop :=
  | box_rel2_box s t U :
      closed s -> [ ⊢ s :- U ] ->
      closed t -> [ ⊢ t :- U ] ->
      (forall ξ, strongly2 (logrel2 P U) s.|[ren ξ] t.|[ren ξ]) ->
      box_rel2 P (Box s) (Box t)
  | box_rel2_tlam s t : box_rel2 P s t -> box_rel2 P (TLam s) (TLam t)
  | box_rel2_tall s t : box_rel2 P s t -> box_rel2 P (TAll s) (TAll t)
  | box_rel2_neu s t : box_rel2 P s t -> box_rel2 P (Neu s) (Neu t)
  | box_rel2_imp s t f : box_rel2 P s t -> box_rel2 P (Imp s f) (Imp t f)
  | box_rel2_lam s t U : box_rel2 P s t -> box_rel2 P (Lam s U) (Lam t U)
  | box_rel2_tapp s t T : box_rel2 P s t -> box_rel2 P (TApp s T) (TApp t T)
  | box_rel2_var x : box_rel2 P (Var x) (Var x)
  | box_rel2_top : box_rel2 P Top Top
  | box_rel2_zero : box_rel2 P Zero Zero
  | box_rel2_app s1 t1 s2 t2 :
      box_rel2 P s1 s2 -> box_rel2 P t1 t2 -> box_rel2 P (App s1 t1) (App s2 t2)
  | box_rel2_and s1 t1 s2 t2 :
      box_rel2 P s1 s2 -> box_rel2 P t1 t2 -> box_rel2 P (And s1 t1) (And s2 t2).

Lemma box_rel2_weight_eq P s t :
  box_rel2 P s t -> weight s = weight t.
Proof.
  by elim=>//=; eauto.
Qed.

Lemma box_rel2_preserved_neu P s t :
  box_rel2 P s t ->
  box_rel2 P (neu s) (neu t).
Proof.
  elim=>{s t}//=; try by constructor.
  move=> s t U hc1 ht1 hc2 ht2 h.
  apply box_rel2_box with U.
  - by apply closed_sneu.
  - by apply has_type_neu.
  - by apply closed_sneu.
  - by apply has_type_neu.
  - move=> θ; rewrite -!neu_hsubst_comm.
    have[??]:= h θ.
    by split; rewrite ?neu_idempotent.
Qed.

Lemma box_rel2_preserved_subst P s t u v U :
  closed u -> [ ⊢ u :- U ] ->
  closed v -> [ ⊢ v :- U ] ->
  (forall ξ, strongly2 (logrel2 P U) u.|[ren ξ] v.|[ren ξ]) ->
  box_rel2 P s t ->
  forall n, box_rel2 P s.[Box u//n] t.[Box v//n].
Proof.
  move=> hcu htu hcv htv hst hb.
  move: u v hcu htu hcv htv hst.
  elim: hb=>{s t}.
  - move=> s t W hc1 ht1 hc2 ht2 hs u v hcu htu hcv htv hst n /=.
    (* the substitution does not enter a box *)
    have->: s.[subst_var (Box u) n] = s by apply closed_subst.
    have->: t.[subst_var (Box v) n] = t by apply closed_subst.
    by apply box_rel2_box with W.
  - move=> s t _ ih u v hcu htu hcv htv hst n /=.
    (* the boxes travel under the binder, so their contents are shifted *)
    rewrite !subst_var_hsubst /=.
    apply box_rel2_tlam; apply ih.
    + by apply closed_unaffectedh.
    + by apply has_type_hsubst_0.
    + by apply closed_unaffectedh.
    + by apply has_type_hsubst_0.
    + by move=> θ; asimpl; apply hst.
  - move=> s t _ ih u v hcu htu hcv htv hst n /=.
    rewrite !subst_var_hsubst /=.
    apply box_rel2_tall; apply ih.
    + by apply closed_unaffectedh.
    + by apply has_type_hsubst_0.
    + by apply closed_unaffectedh.
    + by apply has_type_hsubst_0.
    + by move=> θ; asimpl; apply hst.
  - move=> s t _ ih u v hcu htu hcv htv hst n /=.
    apply box_rel2_neu.
    by apply ih.
  - move=> s t f _ ih u v hcu htu hcv htv hst n /=.
    apply box_rel2_imp.
    by apply ih.
  - move=> s t W _ ih u v hcu htu hcv htv hst n /=.
    rewrite upn1 !subst_var_lemma.
    have->: (Box u).[ren (+1)] = Box u by apply closed_subst, closed_box.
    have->: (Box v).[ren (+1)] = Box v by apply closed_subst, closed_box.
    apply box_rel2_lam. by apply ih.
  - move=> s t T _ ih u v hcu htu hcv htv hst n /=.
    apply box_rel2_tapp.
    by apply ih.
  - move=> x u v hcu htu hcv htv hst n /=.
    rewrite /subst_var.
    case (lt_eq_lt_dec x n)=> [[]|] hn; try by apply box_rel2_var.
    by apply box_rel2_box with U.
  - by move=> *; apply box_rel2_top.
  - by move=> *; apply box_rel2_zero.
  - move=> s1 t1 s2 t2 _ ih1 _ ih2 u v hcu htu hcv htv hst n /=.
    apply box_rel2_app; by [apply ih1 | apply ih2].
  - move=> s1 t1 s2 t2 _ ih1 _ ih2 u v hcu htu hcv htv hst n /=.
    apply box_rel2_and; by [apply ih1 | apply ih2].
Qed.

Corollary box_rel2_preserved_subst0 P s t u v U :
  closed u -> [ ⊢ u :- U ] ->
  closed v -> [ ⊢ v :- U ] ->
  (forall ξ, strongly2 (logrel2 P U) u.|[ren ξ] v.|[ren ξ]) ->
  box_rel2 P s t ->
  box_rel2 P s.[Box u/] t.[Box v/].
Proof.
  move=> *.
  have:= @box_rel2_preserved_subst P s t u v U.
  rewrite -!subst_var_0.
  by apply.
Qed.

Lemma box_rel2_preserved_ren P s t :
  box_rel2 P s t ->
  forall ξ, box_rel2 P s.|[ren ξ] t.|[ren ξ].
Proof.
  elim=>{s t}.
  - move=> s t U hc1 ht1 hc2 ht2 hs θ /=.
    apply box_rel2_box with U=> [||||θ'].
    + by apply closed_unaffectedh.
    + by apply has_type_hsubst_0.
    + by apply closed_unaffectedh.
    + by apply has_type_hsubst_0.
    + by asimpl.
  - move=> s t _ ih θ /=.
    rewrite !up_ren_term.
    apply box_rel2_tlam.
    by apply ih.
  - move=> s t _ ih θ /=.
    rewrite !up_ren_term.
    apply box_rel2_tall.
    by apply ih.
  - move=> s t _ ih θ /=. apply box_rel2_neu. by apply ih.
  - move=> s t f _ ih θ /=. apply box_rel2_imp. by apply ih.
  - move=> s t U _ ih θ /=. apply box_rel2_lam. by apply ih.
  - move=> s t T _ ih θ /=. apply box_rel2_tapp. by apply ih.
  - by move=> x θ /=; apply box_rel2_var.
  - by move=> θ /=; apply box_rel2_top.
  - by move=> θ /=; apply box_rel2_zero.
  - move=> s1 t1 s2 t2 _ ih1 _ ih2 θ /=.
    apply box_rel2_app; by [apply ih1 | apply ih2].
  - move=> s1 t1 s2 t2 _ ih1 _ ih2 θ /=.
    apply box_rel2_and; by [apply ih1 | apply ih2].
Qed.

Lemma box_rel2_preserved_hsubst P r1 r2 Γ U1 U2 a b d T :
  d < b ->
  [ Γ, a, b ⊢ r1 :- U1 ] -> [ Γ, a, b ⊢ r2 :- U2 ] ->
  box_rel2 P r1 r2 ->
  box_rel2 P r1.|[upn d (T .: ids)] r2.|[upn d (T .: ids)].
Proof.
  move=> hdb ht1 ht2 hb.
  move: hb Γ U1 U2 a b d hdb ht1 ht2.
  elim=>{r1 r2}.
  - move=> s t V hcs hts hct htt hst Γ U1 U2 a b d hdb ht1 ht2 /=.
    inv ht1.
    inv ht2.
    rewrite (hsubst_T_is_ren (Γ:=Γ) (U:=U1) (a:=0) (b:=b) (s:=s))=>//.
    rewrite (hsubst_T_is_ren (Γ:=Γ) (U:=U2) (a:=0) (b:=b) (s:=t))=>//.
    apply box_rel2_box with V=> [||||ξ'].
    + by apply closed_unaffectedh.
    + by apply has_type_hsubst_0.
    + by apply closed_unaffectedh.
    + by apply has_type_hsubst_0.
    + by asimpl.
  - move=> s t _ ih Γ U1 U2 a b d hdb ht1 ht2 /=.
    inv ht1.
    inv ht2.
    rewrite !fold_up_upn.
    apply box_rel2_tlam.
    apply ih with Γ U U0 a.+1 b.+1=>//.
  - move=> s t _ ih Γ U1 U2 a b d hdb ht1 ht2 /=.
    inv ht1.
    inv ht2.
    rewrite !fold_up_upn.
    apply box_rel2_tall.
    apply ih with Γ Void Void a.+1 b.+1=>//.
  - move=> s t _ ih Γ U1 U2 a b d hdb ht1 ht2 /=.
    inv ht1.
    inv ht2.
    apply box_rel2_neu.
    by apply ih with Γ U1 U2 a b.
  - move=> s t f _ ih Γ U1 U2 a b d hdb ht1 ht2 /=.
    inv ht1.
    inv ht2.
    apply box_rel2_imp.
    by apply ih with Γ Void Void a b.
  - move=> s t W _ ih Γ U1 U2 a b d hdb ht1 ht2 /=.
    inv ht1.
    inv ht2.
    apply box_rel2_lam.
    by apply ih with (W .: Γ) V V0 a b.
  - move=> s t S _ ih Γ U1 U2 a b d hdb ht1 ht2 /=.
    inv ht1.
    inv ht2.
    apply box_rel2_tapp.
    by apply ih with Γ (TArr U1) (TArr U2) a b.
  - by move=> *; apply box_rel2_var.
  - by move=> *; apply box_rel2_top.
  - by move=> *; apply box_rel2_zero.
  - move=> s1 t1 s2 t2 _ ih1 _ ih2 Γ U1 U2 a b d hdb ht1 ht2 /=.
    inv ht1.
    inv ht2.
    apply box_rel2_app; by [apply ih1 with Γ (Arr U U1) (Arr U0 U2) a b|apply ih2 with Γ U U0 a b].
  - move=> s1 t1 s2 t2 _ ih1 _ ih2 Γ U1 U2 a b d hdb ht1 ht2 /=.
    inv ht1.
    inv ht2.
    apply box_rel2_and; by [apply ih1 with Γ U1 U2 a b|apply ih2 with Γ U1 U2 a b].
Qed.

Corollary box_rel2_preserved_hsubst0 P r1 r2 Γ U1 U2 a b T :
  1 <= b ->
  [ Γ, a, b ⊢ r1 :- U1 ] -> [ Γ, a, b ⊢ r2 :- U2 ] ->
  box_rel2 P r1 r2 ->
  box_rel2 P r1.|[T/] r2.|[T/].
Proof.
  move=> hb ht1 ht2 h.
  have:= @box_rel2_preserved_hsubst P r1 r2 Γ U1 U2 a b 0 T.
  rewrite upn0. by apply.
Qed.

Lemma box_rel2_type_det P s t Γ U1 U2 a b :
  box_rel2 P s t ->
  [ Γ, a, b ⊢ s :- U1 ] -> [ Γ, a, b ⊢ t :- U2 ] ->
  U1 = U2.
Proof.
  move=> hb.
  move: Γ U1 U2 a b.
  elim: hb=>{s t}.
  - move=> s t V hcs hts hct htt _ Γ U1 U2 a b h1 h2.
    inv h1.
    inv h2.
    have e1: U1 = V.
    { apply has_type_det with empty_ctx 0 0 s=>//.
      apply (has_type_lower_b (b:=b))=>//.
      by apply closed_has_ty_contr with Γ. }
    have e2: U2 = V.
    { apply has_type_det with empty_ctx 0 0 t=>//.
      apply (has_type_lower_b (b:=b))=>//.
      by apply closed_has_ty_contr with Γ. }
    by rewrite e1 e2.
  - move=> s t _ ih Γ U1 U2 a b h1 h2.
    inv h1.
    inv h2.
    f_equal.
    by apply ih with (Γ:=Γ) (a:=a.+1) (b:=b.+1).
  - by move=> s t _ ih Γ U1 U2 a b h1 h2; inv h1; inv h2.
  - move=> s t _ ih Γ U1 U2 a b h1 h2.
    inv h1.
    inv h2.
    by apply ih with (Γ:=Γ) (a:=a) (b:=b).
  - by move=> s t f _ ih Γ U1 U2 a b h1 h2; inv h1; inv h2.
  - move=> s t W _ ih Γ U1 U2 a b h1 h2.
    inv h1.
    inv h2.
    f_equal.
    by apply ih with (Γ:=W .: Γ) (a:=a) (b:=b).
  - move=> s t S _ ih Γ U1 U2 a b h1 h2.
    inv h1.
    inv h2.
    have e: TArr U1 = TArr U2 by apply ih with (Γ:=Γ) (a:=a) (b:=b).
    by inv e.
  - by move=> x Γ U1 U2 a b h1 h2; inv h1; inv h2.
  - by move=> Γ U1 U2 a b h1 h2; inv h1; inv h2.
  - by move=> Γ U1 U2 a b h1 h2; inv h1; inv h2.
  - move=> s1 t1 s2 t2 _ ih1 _ ih2 Γ U1 U2 a b h1 h2.
    inv h1.
    inv h2.
    have e: Arr U U1 = Arr U0 U2 by apply ih1 with (Γ:=Γ) (a:=a) (b:=b).
    by inv e.
  - move=> s1 t1 s2 t2 _ ih1 _ ih2 Γ U1 U2 a b h1 h2.
    inv h1.
    inv h2.
    by apply ih1 with (Γ:=Γ) (a:=a) (b:=b).
Qed.

Lemma box_rel2_box_ids P s t :
  box_rel2 P (Box s) (Box t) ->
  exists U, closed s /\ [ ⊢ s :- U ] /\
            closed t /\ [ ⊢ t :- U ] /\
            strongly2 (logrel2 P U) s t.
Proof.
  move=> h; inv h.
  exists U; do 4 (split=>//).
  have hh: strongly2 (logrel2 P U) s.|[ids] t.|[ids] by apply H5.
  by asimpl in hh.
Qed.

Lemma box_rel2_nobox P s :
  ~ mem_box s -> box_rel2 P s s.
Proof.
  elim: s
    => [x|||s hs t ht|s hs t ht|s hs S|s hs W|s hs f|s hs|s hs|s hs|s hs] /= h;
    try by constructor.
  - constructor; by [apply hs=> ?; apply h; left | apply ht=> ?; apply h; right].
  - constructor; by [apply hs=> ?; apply h; left | apply ht=> ?; apply h; right].
  - by constructor; apply hs.
  - by constructor; apply hs.
  - by constructor; apply hs.
  - by constructor; apply hs.
  - by constructor; apply hs.
  - by constructor; apply hs.
  - by exfalso; apply h.
Qed.