Rocoma.Recipes_fusion

Fusion and meet (TOPLAS 3.7 to 3.10)



Section Sem.

Open Scope valid_scope.

Ltac definitions do not survive the end of a section.
Ltac valid_trivial :=
  by first [ apply valid_top
           | apply valid_top0
           | apply valid_contradiction
           | apply valid_assumption
           | apply valid_assumption_and ].

Ltac tac_valid :=
 first [ done | valid_trivial
       | do 1 apply valid_weak; valid_trivial
       | do 2 apply valid_weak; valid_trivial
       | do 3 apply valid_weak; valid_trivial
       | apply valid_and_l_sym; valid_trivial
       | apply valid_and_l_weak2; valid_trivial
       ].

Ltac tac_valid_cut c :=
  apply valid_cut with c; tac_valid.

wrong definition: on weakened complete recipes this is always true neu s = Top = neu t, when s t : Void
Definition equivalent s t := entails s t /\ entails t s.

Definition EQU U s t := ENT U s t /\ ENT U t s.

Definition strongly3 (R : recipe -> recipe -> recipe -> Prop) r s t :=
  R r s t /\ R (neu r) (neu s) (neu t).

logrel3 requires weak equivalence
Fixpoint logrel3 R U r s t : Prop :=
  EQU U (neu s) (neu t) /\
  match U with
  | Void => R r s t
  | Arr U V =>
      forall t1 t2 t3,
        closed t1 -> [ ⊢ t1 :- U ] ->
        closed t2 -> [ ⊢ t2 :- U ] ->
        closed t3 -> [ ⊢ t3 :- U ] ->
        (forall ξ, strongly3 (logrel3 R U) t1.|[ren ξ] t2.|[ren ξ] t3.|[ren ξ]) ->
        logrel3 R V (App r t1) (App s t2) (App t t3)
  | TArr V =>
      forall T, logrel3 R V (TApp r T) (TApp s T) (TApp t T)
  end.

Lemma logrel3_andl R U r s t :
  logrel3 R U r s t -> EQU U (neu s) (neu t).
Proof.
  elim: U.
  - by move=> > [].
  - by move=> ?? ?? > [].
  - by move=> ?? > [].
Qed.

The weak equivalence carried by logrel3, read on the arguments of the binary clause.
Lemma logrel3_andl_ren R U t1 t2 t3 :
  (forall ξ, strongly3 (logrel3 R U) t1.|[ren ξ] t2.|[ren ξ] t3.|[ren ξ]) ->
  (forall ξ, strongly2 (logrel2 entails U) (neu t2).|[ren ξ] (neu t3).|[ren ξ]) /\
  (forall ξ, strongly2 (logrel2 entails U) (neu t3).|[ren ξ] (neu t2).|[ren ξ]).
Proof.
  move=> h.
  split=> ξ; have [/logrel3_andl [h1 h2] _] := h ξ;
    rewrite -!neu_hsubst_comm; split; rewrite ?neu_idempotent=>//.
Qed.

Inductive stack_rel3 P : type -> stack -> stack -> stack -> Prop :=
| stack_rel3_nil :
    stack_rel3 P Void [::] [::] [::]
| stack_rel3_term t l1 l2 l3 U :
    stack_rel3 P U l1 l2 l3 ->
    stack_rel3 P (TArr U) (T t :: l1) (T t :: l2) (T t :: l3)
| stack_rel3_recipe r s t l1 l2 l3 U V :
    (forall ξ, strongly3 (logrel3 P U) r.|[ren ξ] s.|[ren ξ] t.|[ren ξ]) ->
    stack_rel3 P V l1 l2 l3 ->
    stack_rel3 P (Arr U V) (R r :: l1) (R s :: l2) (R t :: l3).

Lemma logical_relation_lemma3 R U r s t :
  closed r -> [ ⊢ r :- U ] ->
  closed s -> [ ⊢ s :- U ] ->
  closed t -> [ ⊢ t :- U ] ->
  logrel3 R U r s t <->
  EQU U (neu s) (neu t) /\
  (forall l1 l2 l3, stack_rel3 R U l1 l2 l3 ->
                    aligned l1 U -> aligned l2 U -> aligned l3 U ->
                    R (r ∘ l1) (s ∘ l2) (t ∘ l3)).
Proof.
  move: R=> P hc1 ht1 hc2 ht2 hc3 ht3.
  rewrite /aligned.
  split.
  { elim: U r s t hc1 ht1 hc2 ht2 hc3 ht3.
    - move=> > ?????? /= [??].
      split=>// > hl ???.
      by inv hl.
    - move=> U h1 V h2 > ?????? /= h.
      split; first by destruct h.
      move=> > hl [ha1 hb1] [ha2 hb2] [ha3 hb3].
      inv hl=>/=.
      inv ha1.
      inv hb1.
      inv ha2.
      inv hb2.
      inv ha3.
      inv hb3.
      apply h2=>//;
        first [ by apply closed_app; split
              | by apply ty_app with U
              | by apply h
              | by split
              | idtac ].
    - move=> V h2 > ?????? /= h.
      split; first by destruct h.
      move=> > hl [ha1 hb1] [ha2 hb2] [ha3 hb3].
      inv hl=>/=.
      inv ha1.
      inv hb1.
      inv ha2.
      inv hb2.
      inv ha3.
      inv hb3.
      apply h2=>//;
        first [ by apply closed_tapp
              | by constructor=>//; apply fv_plage_eq
              | by apply h
              | by split
              | idtac ]. }
  { elim: U r s t hc1 ht1 hc2 ht2 hc3 ht3.
    - move=> > ?????? [h1 h2].
      repeat split.
      + by destruct h1.
      + by destruct h1.
      + apply: (h2 [::] [::] [::]); by [constructor|split; constructor].
    - move=> U h1 V h2 r s t ?????? [hh1 hh2].
      split=>// u v w ?????? huvw.
      apply h2;
        first [ by apply closed_app; split
              | by apply ty_app with U
              | idtac ].
      split=>/=.
      + have [huv hwv] := logrel3_andl_ren huvw.
        split.
        * apply hh1=>//; by [apply closed_sneu|apply has_type_neu].
        * apply hh1=>//; by [apply closed_sneu|apply has_type_neu].
      + move=> l1 l2 l3 hl [??] [??] [??].
        have->: App r u ∘ l1 = r ∘ (R u :: l1) by [].
        have->: App s v ∘ l2 = s ∘ (R v :: l2) by [].
        have->: App t w ∘ l3 = t ∘ (R w :: l3) by [].
        apply hh2; by [constructor|split; constructor].
    - move=> V h2 r s t ?????? [h0 h].
      split=>//= S.
      apply h2=>//;
        first [ by apply closed_tapp
              | by constructor=>//; apply fv_plage_eq
              | idtac ].
      split=>/=.
      + by split; apply h0.
      + move=> l1 l2 l3 hl [??] [??] [??].
        have->: TApp r S ∘ l1 = r ∘ (T S :: l1) by [].
        have->: TApp s S ∘ l2 = s ∘ (T S :: l2) by [].
        have->: TApp t S ∘ l3 = t ∘ (T S :: l3) by [].
        apply h; by [constructor|split; constructor=>//; apply fv_plage_eq]. }
Qed.

Corollary logical_relation_lemma3_proj1 R U r s t :
  logrel3 R U r s t ->
  forall l1 l2 l3,
  closed r -> [ ⊢ r :- U ] ->
  closed s -> [ ⊢ s :- U ] ->
  closed t -> [ ⊢ t :- U ] ->
  stack_rel3 R U l1 l2 l3 -> aligned l1 U -> aligned l2 U -> aligned l3 U ->
  R (r ∘ l1) (s ∘ l2) (t ∘ l3).
Proof.
  move=> h l1 l2 l3 hc1 ht1 hc2 ht2 hc3 ht3.
  by apply (proj2 (proj1 (logical_relation_lemma3 R hc1 ht1 hc2 ht2 hc3 ht3) h)).
Qed.

Corollary logical_relation_lemma3_proj2 R U r s t :
  EQU U (neu s) (neu t) ->
  (forall l1 l2 l3, stack_rel3 R U l1 l2 l3 ->
                    aligned l1 U -> aligned l2 U -> aligned l3 U ->
                    R (r ∘ l1) (s ∘ l2) (t ∘ l3)) ->
  closed r -> [ ⊢ r :- U ] ->
  closed s -> [ ⊢ s :- U ] ->
  closed t -> [ ⊢ t :- U ] ->
  logrel3 R U r s t.
Proof.
  move=> h1 h2 hc1 ht1 hc2 ht2 hc3 ht3.
  by apply (proj2 (logical_relation_lemma3 R hc1 ht1 hc2 ht2 hc3 ht3)).
Qed.

Fusion (TOPLAS page 13)

Syntactic only, and under boxes.
Inductive fusion : recipe -> recipe -> recipe -> Prop :=
| fus_var x :
    fusion (Var x) (Var x) (Var x)
| fus_top :
    fusion Top Top Top
| fus_zero :
    fusion Zero Zero Zero
| fus_zero1 :
    fusion Zero Top Zero
| fus_zero2 :
    fusion Zero Zero Top
| fus_imp r s t f :
    fusion r s t ->
    fusion (Imp r f) (Imp s f) (Imp t f)
| fus_and r1 s1 t1 r2 s2 t2 :
    fusion r1 s1 t1 ->
    fusion r2 s2 t2 ->
    fusion (And r1 r2) (And s1 s2) (And t1 t2)
| fus_box r s t (*Γ U*) :
    fusion r s t ->
    fusion (Box r) (Box s) (Box t)
| fus_neu r s t :
    fusion r s t ->
    fusion (Neu r) (Neu s) (Neu t)
| fus_tlam r s t :
    fusion r s t ->
    fusion (TLam r) (TLam s) (TLam t)
| fus_tall r s t :
    fusion r s t ->
    fusion (TAll r) (TAll s) (TAll t)
| fus_lam r s t U :
    fusion r s t ->
    fusion (Lam r U) (Lam s U) (Lam t U)
| fus_app r1 s1 t1 r2 s2 t2 :
    fusion r1 s1 t1 ->
    fusion r2 s2 t2 ->
    fusion (App r1 r2) (App s1 s2) (App t1 t2)
| fus_tapp r s t T :
    fusion r s t ->
    fusion (TApp r T) (TApp s T) (TApp t T).

Lemma fusion_refl r :
  fusion r r r.
Proof.
  elim: r; by constructor.
Qed.

Lemma fusion_swap r s t :
  fusion r s t ->
  fusion r t s.
Proof.
  elim: r s t;
    first [ move=> ?????? h
          | move=> ????? h
          | move=> ???? h
          | move=> ??? h
          | move=> ?? h ];
    inv h;
    by (constructor; eauto).
Qed.

Lemma fusion_refl_neu r :
  fusion r r (neu r).
Proof.
  elim: r; by constructor.
Qed.

Lemma fusion_preserved_neu r s t :
  fusion r s t ->
  fusion (neu r) (neu s) (neu t).
Proof.
  elim: r s t.
  - move=> ??? h. inv h. by apply fusion_refl.
  - move=> ?? h. inv h=>/=; by constructor.
  - move=> ?? h. inv h=>/=; by constructor.
  - move=> s h1 t h2 u v h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 t h2 u v h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 ? u v h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 ? u v h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 ? u v h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 u v h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 u v h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 u v h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 u v h. inv h=>/=.
    injections.
    by constructor; eauto.
Qed.

Lemma fusion_preserved_hsubst r s t θ :
  fusion r s t ->
  fusion r.|[θ] s.|[θ] t.|[θ].
Proof.
  elim: r s t θ.
  - move=> ???? h. inv h. by apply fusion_refl.
  - move=> ??? h. inv h=>/=; by constructor.
  - move=> ??? h. inv h=>/=. by constructor.
  - move=> s h1 t h2 u v θ h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 t h2 u v θ h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 ? u v θ h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 ? u v θ h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 ? u v θ h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 u v θ h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 u v θ h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 u v θ h. inv h=>/=.
    injections.
    by constructor; eauto.
  - move=> s h1 u v θ h. inv h=>/=.
    injections.
    by constructor; eauto.
Qed.

Lemma fusion_db3_fusion u v w r s t :
  fusion r s t ->
  db3 u v w r s t ->
  fusion u v w.
Proof.
  elim: r s t u v w.
  - move=> > ? hdb. by inv hdb.
  - move=> > ? hdb. by inv hdb.
  - move=> > ? hdb. by inv hdb.
  - move=> ???? > hfus hdb.
    inv hdb; injections; inv hfus; by eauto.
  - move=> ???? > hfus hdb.
    inv hdb; injections; inv hfus; by eauto.
  - move=> ?? > hfus hdb.
    inv hdb; injections; inv hfus; by eauto.
  - move=> ?? > hfus hdb.
    inv hdb; injections; inv hfus; by eauto.
  - move=> ?? > hfus hdb.
    inv hdb; injections; inv hfus; by eauto.
  - move=> ?? > hfus hdb.
    inv hdb; injections; inv hfus; by eauto.
  - move=> ?? > hfus hdb.
    inv hdb; injections; inv hfus; by eauto.
  - move=> ?? > hfus hdb.
    inv hdb; injections; inv hfus; by eauto.
  - move=> ?? > hfus hdb.
    inv hdb; injections; inv hfus. done.
Qed.

Lemma fusion_fv r s t n :
  fv n r ->
  fusion r s t ->
  fv n s.
Proof.
  elim: r s t n.
  - move=> > ? hfus. by inv hfus.
  - move=> > ? hfus. by inv hfus.
  - move=> > ? hfus. by inv hfus.
  - move=> s h1 t h2 > /fv_and [??] hfus. inv hfus. by apply fv_and; eauto.
  - move=> s h1 t h2 > /fv_app [??] hfus. inv hfus. apply fv_app; by eauto.
  - move=> s h1 > /fv_tapp ? hfus. inv hfus. apply fv_tapp; by eauto.
  - move=> s h1 > /fv_lam ? hfus. inv hfus. apply fv_lam; by eauto.
  - move=> s h1 > /fv_imp ? hfus. inv hfus. apply fv_imp; by eauto.
  - move=> s h1 > /fv_tlam ? hfus. inv hfus. apply fv_tlam; by eauto.
  - move=> s h1 > /fv_tall ? hfus. inv hfus. apply fv_tall; by eauto.
  - move=> s h1 > /fv_neu ? hfus. inv hfus. apply fv_neu; by eauto.
  - move=> s h1 > /fv_box ? hfus. inv hfus. apply fv_box. by eauto.
Qed.

Corollary fusion_closed r s t :
  closed r ->
  fusion r s t ->
  closed s.
Proof.
  rewrite !/closed.
  by apply fusion_fv.
Qed.

Lemma fusion_has_type r s t Γ U a b :
  [ Γ, a, b ⊢ r :- U ] ->
  fusion r s t ->
  [ Γ, a, b ⊢ s :- U ].
Proof.
  elim: r s t Γ U a b.
  - move=> > ? hf. by inv hf.
  - move=> > ht hf. inv ht; inv hf; by constructor.
  - move=> > ht hf. inv ht; inv hf; by constructor.
  - move=> s h1 t h2 > ht hf. inv ht. inv hf. constructor; by eauto.
  - move=> s h1 t h2 > ht hf. inv ht. inv hf. apply ty_app with U; by eauto.
  - move=> s h1 > ht hf. inv ht. inv hf. constructor; by eauto.
  - move=> s h1 > ht hf. inv ht. inv hf. constructor; by eauto.
  - move=> s h1 > ht hf. inv ht. inv hf. constructor; by eauto.
  - move=> s h1 > ht hf. inv ht. inv hf. constructor; by eauto.
  - move=> s h1 > ht hf. inv ht. inv hf. constructor; by eauto.
  - move=> s h1 > ht hf. inv ht. inv hf. constructor; by eauto.
  - move=> s h1 > ht hf. inv ht. inv hf. constructor.
    by apply fusion_closed with s t.
    by apply h1 with t.
Qed.

Inductive box_rel3 R : recipe -> recipe -> recipe -> Prop :=
| box_rel3_box r s t U :
    closed r -> [ ⊢ r :- U ] ->
    closed s -> [ ⊢ s :- U ] ->
    closed t -> [ ⊢ t :- U ] ->
    (forall ξ, strongly3 (logrel3 R U) r.|[ren ξ] s.|[ren ξ] t.|[ren ξ]) ->
    box_rel3 R (Box r) (Box s) (Box t)
| box_rel3_tlam r s t : box_rel3 R r s t -> box_rel3 R (TLam r) (TLam s) (TLam t)
| box_rel3_tall r s t : box_rel3 R r s t -> box_rel3 R (TAll r) (TAll s) (TAll t)
| box_rel3_neu r s t : box_rel3 R r s t -> box_rel3 R (Neu r) (Neu s) (Neu t)
| box_rel3_imp r s t f : box_rel3 R r s t -> box_rel3 R (Imp r f) (Imp s f) (Imp t f)
| box_rel3_lam r s t U : box_rel3 R r s t -> box_rel3 R (Lam r U) (Lam s U) (Lam t U)
| box_rel3_tapp r s t T : box_rel3 R r s t -> box_rel3 R (TApp r T) (TApp s T) (TApp t T)
| box_rel3_var x : box_rel3 R (Var x) (Var x) (Var x)
| box_rel3_top : box_rel3 R Top Top Top
| box_rel3_zeroz : box_rel3 R Zero Zero Zero
| box_rel3_zerol : box_rel3 R Zero Top Zero
| box_rel3_zeror : box_rel3 R Zero Zero Top
| box_rel3_app r1 s1 t1 r2 s2 t2 :
    box_rel3 R r1 s1 t1 -> box_rel3 R r2 s2 t2 ->
    box_rel3 R (App r1 r2) (App s1 s2) (App t1 t2)
| box_rel3_and r1 s1 t1 r2 s2 t2 :
    box_rel3 R r1 s1 t1 -> box_rel3 R r2 s2 t2 ->
    box_rel3 R (And r1 r2) (And s1 s2) (And t1 t2).

Lemma box_rel3_nobox R r s t :
  fusion r s t -> ~ mem_box r -> box_rel3 R r s t.
Proof.
  elim=>{r s t}//= > ; try by constructor.
  - move=> _ ih h.
    by constructor; apply ih.
  - move=> _ ih1 _ ih2 h.
    constructor; by [apply ih1=> ?; apply h; left | apply ih2=> ?; apply h; right].
  - move=> _ ih h.
    by constructor; apply ih.
  - move=> _ ih h.
    by constructor; apply ih.
  - move=> _ ih h.
    by constructor; apply ih.
  - move=> _ ih h.
    by constructor; apply ih.
  - move=> _ ih1 _ ih2 h.
    constructor; by [apply ih1=> ?; apply h; left | apply ih2=> ?; apply h; right].
  - move=> _ ih h.
    by constructor; apply ih.
Qed.

Lemma box_rel3_preserved_neu R r s t :
  box_rel3 R r s t ->
  box_rel3 R (neu r) (neu s) (neu t).
Proof.
  elim=>{r s t}//=; try by constructor.
  move=> r s t U hcr htr hcs hts hct htt h.
  apply box_rel3_box with U;
    try by [apply closed_sneu|apply has_type_neu].
  move=> ξ; rewrite -!neu_hsubst_comm.
  have[??]:= h ξ.
  by split; rewrite ?neu_idempotent.
Qed.

Lemma box_rel3_preserved_subst R r s t u v w U :
  closed u -> [ ⊢ u :- U ] ->
  closed v -> [ ⊢ v :- U ] ->
  closed w -> [ ⊢ w :- U ] ->
  (forall ξ, strongly3 (logrel3 R U) u.|[ren ξ] v.|[ren ξ] w.|[ren ξ]) ->
  box_rel3 R r s t ->
  forall n, box_rel3 R r.[Box u//n] s.[Box v//n] t.[Box w//n].
Proof.
  move=> hcu htu hcv htv hcw htw hst hb.
  move: u v w hcu htu hcv htv hcw htw hst.
  elim: hb=>{r s t}.
  - move=> r s t W hc1 ht1 hc2 ht2 hc3 ht3 hs u v w hcu htu hcv htv hcw htw hst n /=.
    rewrite !closed_subst=>//.
    by apply box_rel3_box with W.
  - move=> r s t _ ih u v w hcu htu hcv htv hcw htw hst n /=.
    (* the boxes travel under the binder, so their contents are shifted *)
    rewrite !subst_var_hsubst /=.
    apply box_rel3_tlam; apply ih;
      try by [apply closed_unaffectedh|apply has_type_hsubst_0].
    by move=> ξ; asimpl; apply hst.
  - move=> r s t _ ih u v w hcu htu hcv htv hcw htw hst n /=.
    rewrite !subst_var_hsubst /=.
    apply box_rel3_tall; apply ih;
      try by [apply closed_unaffectedh|apply has_type_hsubst_0].
    by move=> ξ; asimpl; apply hst.
  - move=> r s t _ ih u v w hcu htu hcv htv hcw htw hst n /=.
    apply box_rel3_neu.
    by apply ih.
  - move=> r s t f _ ih u v w hcu htu hcv htv hcw htw hst n /=.
    apply box_rel3_imp.
    by apply ih.
  - move=> r s t W _ ih u v w hcu htu hcv htv hcw htw 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.
    have->: (Box w).[ren (+1)] = Box w by apply closed_subst, closed_box.
    apply box_rel3_lam.
    by apply ih.
  - move=> r s t T _ ih u v w hcu htu hcv htv hcw htw hst n /=.
    apply box_rel3_tapp.
    by apply ih.
  - move=> x u v w hcu htu hcv htv hcw htw hst n /=.
    rewrite /subst_var.
    case (lt_eq_lt_dec x n)=> [[]|] hn; try by apply box_rel3_var.
    by apply box_rel3_box with U.
  - by move=> *; apply box_rel3_top.
  - by move=> *; apply box_rel3_zeroz.
  - by move=> *; apply box_rel3_zerol.
  - by move=> *; apply box_rel3_zeror.
  - move=> r1 s1 t1 r2 s2 t2 _ ih1 _ ih2 u v w hcu htu hcv htv hcw htw hst n /=.
    apply box_rel3_app; by [apply ih1|apply ih2].
  - move=> r1 s1 t1 r2 s2 t2 _ ih1 _ ih2 u v w hcu htu hcv htv hcw htw hst n /=.
    apply box_rel3_and; by [apply ih1|apply ih2].
Qed.

Corollary box_rel3_preserved_subst0 R r s t u v w U :
  closed u -> [ ⊢ u :- U ] ->
  closed v -> [ ⊢ v :- U ] ->
  closed w -> [ ⊢ w :- U ] ->
  (forall ξ, strongly3 (logrel3 R U) u.|[ren ξ] v.|[ren ξ] w.|[ren ξ]) ->
  box_rel3 R r s t ->
  box_rel3 R r.[Box u/] s.[Box v/] t.[Box w/].
Proof.
  move=> *.
  have:= @box_rel3_preserved_subst R r s t u v w U.
  rewrite -!subst_var_0.
  by apply.
Qed.

Lemma box_rel3_preserved_ren R r s t :
  box_rel3 R r s t ->
  forall ξ, box_rel3 R r.|[ren ξ] s.|[ren ξ] t.|[ren ξ].
Proof.
  elim=>{r s t}.
  - move=> r s t U hc1 ht1 hc2 ht2 hc3 ht3 hs ξ /=.
    apply box_rel3_box with U=> [||||||ξ'];
      try by [apply closed_unaffectedh|apply has_type_hsubst_0].
    by asimpl.
  - move=> r s t _ ih ξ /=.
    rewrite !up_ren_term.
    apply box_rel3_tlam.
    by apply ih.
  - move=> r s t _ ih ξ /=.
    rewrite !up_ren_term.
    apply box_rel3_tall.
    by apply ih.
  - move=> r s t _ ih ξ /=.
    apply box_rel3_neu.
    by apply ih.
  - move=> r s t f _ ih ξ /=.
    apply box_rel3_imp.
    by apply ih.
  - move=> r s t U _ ih ξ /=.
    apply box_rel3_lam.
    by apply ih.
  - move=> r s t T _ ih ξ /=.
    apply box_rel3_tapp.
    by apply ih.
  - by move=> x ξ /=; apply box_rel3_var.
  - by move=> ξ /=; apply box_rel3_top.
  - by move=> ξ /=; apply box_rel3_zeroz.
  - by move=> ξ /=; apply box_rel3_zerol.
  - by move=> ξ /=; apply box_rel3_zeror.
  - move=> r1 s1 t1 r2 s2 t2 _ ih1 _ ih2 ξ /=.
    apply box_rel3_app; by [apply ih1|apply ih2].
  - move=> r1 s1 t1 r2 s2 t2 _ ih1 _ ih2 ξ /=.
    apply box_rel3_and; by [apply ih1|apply ih2].
Qed.

Lemma box_rel3_preserved_hsubst R r1 r2 r3 Γ U1 U2 U3 a b d T :
  d < b ->
  [ Γ, a, b ⊢ r1 :- U1 ] -> [ Γ, a, b ⊢ r2 :- U2 ] -> [ Γ, a, b ⊢ r3 :- U3 ] ->
  box_rel3 R r1 r2 r3 ->
  box_rel3 R r1.|[upn d (T .: ids)] r2.|[upn d (T .: ids)] r3.|[upn d (T .: ids)].
Proof.
  move=> hdb ht1 ht2 ht3 hb.
  move: hb Γ U1 U2 U3 a b d hdb ht1 ht2 ht3.
  elim=>{r1 r2 r3}.
  - move=> r s t V hcr htr hcs hts hct htt hst Γ U1 U2 U3 a b d hdb ht1 ht2 ht3 /=.
    inv ht1. inv ht2. inv ht3.
    rewrite (hsubst_T_is_ren (Γ:=Γ) (U:=U1) (a:=0) (b:=b) (s:=r))=>//.
    rewrite (hsubst_T_is_ren (Γ:=Γ) (U:=U2) (a:=0) (b:=b) (s:=s))=>//.
    rewrite (hsubst_T_is_ren (Γ:=Γ) (U:=U3) (a:=0) (b:=b) (s:=t))=>//.
    apply box_rel3_box with V=> [||||||ξ'];
      try by [apply closed_unaffectedh|apply has_type_hsubst_0].
    by asimpl.
  - move=> r s t _ ih Γ U1 U2 U3 a b d hdb ht1 ht2 ht3 /=.
    inv ht1.
    inv ht2.
    inv ht3.
    rewrite !fold_up_upn.
    apply box_rel3_tlam.
    by apply ih with Γ U U0 U1 a.+1 b.+1.
  - move=> r s t _ ih Γ U1 U2 U3 a b d hdb ht1 ht2 ht3 /=.
    inv ht1.
    inv ht2.
    inv ht3.
    rewrite !fold_up_upn.
    apply box_rel3_tall.
    by apply ih with Γ Void Void Void a.+1 b.+1.
  - move=> r s t _ ih Γ U1 U2 U3 a b d hdb ht1 ht2 ht3 /=.
    inv ht1.
    inv ht2.
    inv ht3.
    apply box_rel3_neu.
    by apply ih with Γ U1 U2 U3 a b.
  - move=> r s t f _ ih Γ U1 U2 U3 a b d hdb ht1 ht2 ht3 /=.
    inv ht1.
    inv ht2.
    inv ht3.
    apply box_rel3_imp.
    by apply ih with Γ Void Void Void a b.
  - move=> r s t W _ ih Γ U1 U2 U3 a b d hdb ht1 ht2 ht3 /=.
    inv ht1.
    inv ht2.
    inv ht3.
    apply box_rel3_lam.
    by apply ih with (W .: Γ) V V0 V1 a b.
  - move=> r s t S _ ih Γ U1 U2 U3 a b d hdb ht1 ht2 ht3 /=.
    inv ht1.
    inv ht2.
    inv ht3.
    apply box_rel3_tapp.
    by apply ih with Γ (TArr U1) (TArr U2) (TArr U3) a b.
  - by move=> *; apply box_rel3_var.
  - by move=> *; apply box_rel3_top.
  - by move=> *; apply box_rel3_zeroz.
  - by move=> *; apply box_rel3_zerol.
  - by move=> *; apply box_rel3_zeror.
  - move=> r1 s1 t1 r2 s2 t2 _ ih1 _ ih2 Γ U1 U2 U3 a b d hdb ht1 ht2 ht3 /=.
    inv ht1. inv ht2. inv ht3.
    apply box_rel3_app;
      by [apply ih1 with Γ (Arr U U1) (Arr U0 U2) (Arr U4 U3) a b|apply ih2 with Γ U U0 U4 a b].
  - move=> r1 s1 t1 r2 s2 t2 _ ih1 _ ih2 Γ U1 U2 U3 a b d hdb ht1 ht2 ht3 /=.
    inv ht1. inv ht2. inv ht3.
    apply box_rel3_and;
      by [apply ih1 with Γ U1 U2 U3 a b|apply ih2 with Γ U1 U2 U3 a b].
Qed.

Corollary box_rel3_preserved_hsubst0 R r1 r2 r3 Γ U1 U2 U3 a b T :
  1 <= b ->
  [ Γ, a, b ⊢ r1 :- U1 ] -> [ Γ, a, b ⊢ r2 :- U2 ] -> [ Γ, a, b ⊢ r3 :- U3 ] ->
  box_rel3 R r1 r2 r3 ->
  box_rel3 R r1.|[T/] r2.|[T/] r3.|[T/].
Proof.
  move=> hb ht1 ht2 ht3 h.
  have:= @box_rel3_preserved_hsubst R r1 r2 r3 Γ U1 U2 U3 a b 0 T.
  rewrite upn0. by apply.
Qed.

Same shape, same context: same type, for each of the two other recipes.
Lemma box_rel3_type_det12 R r s t Γ U1 U2 a b :
  box_rel3 R r s t ->
  [ Γ, a, b ⊢ r :- U1 ] -> [ Γ, a, b ⊢ s :- U2 ] ->
  U1 = U2.
Proof.
  move=> hb.
  move: Γ U1 U2 a b.
  elim: hb=>{r s t}.
  - move=> r s t V hcr htr hcs hts hct htt _ Γ U1 U2 a b h1 h2.
    inv h1.
    inv h2.
    have e: forall u W, closed u -> [ Γ, 0, b ⊢ u :- W ] -> [ ⊢ u :- V ] -> W = V.
    { move=> u W hc hu hv.
      apply has_type_det with empty_ctx 0 0 u=>//.
      apply (has_type_lower_b (b:=b))=>//.
      by apply closed_has_ty_contr with Γ. }
    by rewrite (e r U1) // (e s U2).
  - move=> r 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=> r s t _ ih Γ U1 U2 a b h1 h2; inv h1; inv h2.
  - move=> r s t _ ih Γ U1 U2 a b h1 h2.
    inv h1.
    inv h2.
    by apply ih with (Γ:=Γ) (a:=a) (b:=b).
  - by move=> r s t f _ ih Γ U1 U2 a b h1 h2; inv h1; inv h2.
  - move=> r 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=> r 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.
  - 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=> r1 s1 t1 r2 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=> r1 s1 t1 r2 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_rel3_type_det13 R r s t Γ U1 U2 a b :
  box_rel3 R r s t ->
  [ Γ, a, b ⊢ r :- U1 ] -> [ Γ, a, b ⊢ t :- U2 ] ->
  U1 = U2.
Proof.
  move=> hb.
  move: Γ U1 U2 a b.
  elim: hb=>{r s t}.
  - move=> r s t V hcr htr hcs hts hct htt _ Γ U1 U2 a b h1 h2.
    inv h1.
    inv h2.
    have e: forall u W, closed u -> [ Γ, 0, b ⊢ u :- W ] -> [ ⊢ u :- V ] -> W = V.
    { move=> u W hc hu hv.
      apply has_type_det with empty_ctx 0 0 u=>//.
      apply (has_type_lower_b (b:=b))=>//.
      by apply closed_has_ty_contr with Γ. }
    by rewrite (e r U1) // (e t U2).
  - move=> r 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=> r s t _ ih Γ U1 U2 a b h1 h2; inv h1; inv h2.
  - move=> r s t _ ih Γ U1 U2 a b h1 h2.
    inv h1.
    inv h2.
    by apply ih with (Γ:=Γ) (a:=a) (b:=b).
  - by move=> r s t f _ ih Γ U1 U2 a b h1 h2; inv h1; inv h2.
  - move=> r 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=> r 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.
  - 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=> r1 s1 t1 r2 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=> r1 s1 t1 r2 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_rel3_box_ids R r s t :
  box_rel3 R (Box r) (Box s) (Box t) ->
  exists U, closed r /\ [ ⊢ r :- U ] /\
            closed s /\ [ ⊢ s :- U ] /\
            closed t /\ [ ⊢ t :- U ] /\
            strongly3 (logrel3 R U) r s t.
Proof.
  move=> h; inv h.
  exists U; do 6 (split=>//).
  have hh: strongly3 (logrel3 R U) r.|[ids] s.|[ids] t.|[ids] by apply H8.
  by asimpl in hh.
Qed.

box_rel3 from the typing of three fused recipes: the obligation is on the directly boxed triples.
Lemma unfold_box_rel3 R r s t Γ U a b :
  [ Γ, a, b ⊢ r :- U ] -> [ Γ, a, b ⊢ s :- U ] -> [ Γ, a, b ⊢ t :- U ] ->
  fusion r s t ->
  (forall u v w V,
   db3 u v w r s t -> [ ⊢ u :- V ] -> [ ⊢ v :- V ] -> [ ⊢ w :- V ] ->
   forall ξ, strongly3 (logrel3 R V) u.|[ren ξ] v.|[ren ξ] w.|[ren ξ]) ->
  box_rel3 R r s t.
Proof.
  elim: r s t Γ U a b.
  - move=> > ??? hf _.
    inv hf; by constructor.
  - move=> > ??? hf _.
    inv hf; by constructor.
  - move=> > ??? hf _.
    inv hf; by constructor.
  - move=> r1 h1 r2 h2 s t Γ U a b ht1 ht2 ht3 hf h.
    inv hf.
    inv ht1.
    inv ht2.
    inv ht3.
    apply box_rel3_and.
    + apply h1 with Γ U a b=>// u v w V hdb.
      apply h.
      by apply db_andl3.
    + apply h2 with Γ U a b=>// u v w V hdb.
      apply h.
      by apply db_andr3.
  - move=> r1 h1 r2 h2 s t Γ U a b ht1 ht2 ht3 hf h.
    inv hf.
    inv ht1.
    have hs1: [ Γ, a, b ⊢ s1 :- Arr U0 U ] by apply fusion_has_type with r1 t1.
    have ht1': [ Γ, a, b ⊢ t1 :- Arr U0 U ].
    { apply fusion_has_type with r1 s1=>//. by apply fusion_swap. }
    have hs2: [ Γ, a, b ⊢ s2 :- U0 ] by apply fusion_has_type with r2 t2.
    have ht2': [ Γ, a, b ⊢ t2 :- U0 ].
    { apply fusion_has_type with r2 s2=>//. by apply fusion_swap. }
    apply box_rel3_app.
    + apply h1 with Γ (Arr U0 U) a b=>// u v w V hdb.
      apply h.
      by apply db_appl3.
    + apply h2 with Γ U0 a b=>// u v w V hdb.
      apply h.
      by apply db_appr3.
  - move=> r h1 S s t Γ U a b ht1 ht2 ht3 hf h.
    inv hf.
    inv ht1.
    inv ht2.
    inv ht3.
    apply box_rel3_tapp.
    apply h1 with Γ (TArr U) a b=>// u v w V hdb.
    apply h.
    by apply db_tapp3.
  - move=> r h1 W s t Γ U a b ht1 ht2 ht3 hf h.
    inv hf.
    inv ht1.
    inv ht2.
    inv ht3.
    apply box_rel3_lam.
    apply h1 with (W .: Γ) V a b=>// u v w V' hdb.
    apply h.
    by apply db_lam3.
  - move=> r h1 f s t Γ U a b ht1 ht2 ht3 hf h.
    inv hf.
    inv ht1.
    inv ht2.
    inv ht3.
    apply box_rel3_imp.
    apply h1 with Γ Void a b=>// u v w V hdb.
    apply h.
    by apply db_imp3.
  - move=> r h1 s t Γ U a b ht1 ht2 ht3 hf h.
    inv hf.
    inv ht1.
    inv ht2.
    inv ht3.
    apply box_rel3_tlam.
    apply h1 with Γ U0 a.+1 b.+1=>// u v w V hdb.
    apply h.
    by apply db_tlam3.
  - move=> r h1 s t Γ U a b ht1 ht2 ht3 hf h.
    inv hf.
    inv ht1.
    inv ht2.
    inv ht3.
    apply box_rel3_tall.
    apply h1 with Γ Void a.+1 b.+1=>// u v w V hdb.
    apply h.
    by apply db_tall3.
  - move=> r h1 s t Γ U a b ht1 ht2 ht3 hf h.
    inv hf.
    inv ht1.
    inv ht2.
    inv ht3.
    apply box_rel3_neu.
    apply h1 with Γ U a b=>// u v w V hdb.
    apply h.
    by apply db_neu3.
  - move=> r _ s t Γ U a b ht1 ht2 ht3 hf h.
    inv hf.
    inv ht1.
    inv ht2.
    inv ht3.
    have htr: [ ⊢ r :- U ].
    { apply (has_type_lower_b (b:=b))=>//.
      by apply closed_has_ty_contr with Γ. }
    have hts: [ ⊢ s0 :- U ].
    { apply (has_type_lower_b (b:=b))=>//.
      by apply closed_has_ty_contr with Γ. }
    have htt: [ ⊢ t0 :- U ].
    { apply (has_type_lower_b (b:=b))=>//.
      by apply closed_has_ty_contr with Γ. }
    apply box_rel3_box with U=>//.
    apply h=>//.
    by apply db_box3.
Qed.

Lemma EQU_Void_neu s t :
  closed s -> [ ⊢ s :- Void ] ->
  closed t -> [ ⊢ t :- Void ] ->
  EQU Void (neu s) (neu t).
Proof.
  move=> ?? ??.
  have h1: NEU Void (neu t) by apply neuneug.
  have h2: NEU Void (neu s) by apply neuneug.
  split=>/= => > *.
  - apply valid_weak0.
    by apply h1.
  - apply valid_weak0.
    by apply h2.
Qed.

Lemma ENT_and U s1 t1 s2 t2 :
  closed s1 -> [ ⊢ s1 :- U ] ->
  closed t1 -> [ ⊢ t1 :- U ] ->
  closed s2 -> [ ⊢ s2 :- U ] ->
  closed t2 -> [ ⊢ t2 :- U ] ->
  ENT U (neu s1) (neu s2) ->
  ENT U (neu t1) (neu t2) ->
  ENT U (neu (And s1 t1)) (neu (And s2 t2)).
Proof.
  move=> ?? ?? ?? ?? h1 h2.
  have ?: closed (neu s1) by apply closed_sneu.
  have ?: closed (neu s2) by apply closed_sneu.
  have ?: closed (neu t1) by apply closed_sneu.
  have ?: closed (neu t2) by apply closed_sneu.
  have ?: [ ⊢ neu s1 :- U ] by apply has_type_neu.
  have ?: [ ⊢ neu s2 :- U ] by apply has_type_neu.
  have ?: [ ⊢ neu t1 :- U ] by apply has_type_neu.
  have ?: [ ⊢ neu t2 :- U ] by apply has_type_neu.
  apply logical_relation_lemma2_proj2=>/=;
    try first [ by apply closed_and; split | by constructor ].
  move=> l1 l2 h12 ha1 ha2 f g
         /eval_move_stack_right hf
         /eval_move_stack_right hg.
  inv hf. inv hg.
  apply valid_and_and_intro.
  - have h: entails (neu s1 ∘ l1) (neu s2 ∘ l2)
      by apply (logical_relation_lemma2_proj1 h1).
    apply h; by apply eval_move_stack_left.
  - have h: entails (neu t1 ∘ l1) (neu t2 ∘ l2)
      by apply (logical_relation_lemma2_proj1 h2).
    apply h; by apply eval_move_stack_left.
Qed.

Lemma ENT_and1 U s t :
  closed s -> [ ⊢ s :- U ] ->
  closed t -> [ ⊢ t :- U ] ->
  logrel2 entails U (And s t) s.
Proof.
  move=>*.
  have?: closed (And s t) by apply closed_and.
  have?: [ ⊢ And s t :- U ] by constructor.
  apply logical_relation_lemma2_proj2=>// l1 l2 h12 ha1 ha2 f g
    /eval_move_stack_right h1
    /eval_move_stack_right h2.
  inv h1.
  apply valid_cut with s2; try tac_valid.
  have: entails (s ∘ l1) (s ∘ l2).
  { apply logical_relation_lemma2_proj1 with U=>//.
    by apply entails_refl. }
  apply=>//; by apply eval_move_stack_left.
Qed.

Lemma ENT_and2 U s t :
  closed s -> [ ⊢ s :- U ] ->
  closed t -> [ ⊢ t :- U ] ->
  logrel2 entails U (And s t) t.
Proof.
  move=>*.
  have?: closed (And s t) by apply closed_and.
  have?: [ ⊢ And s t :- U ] by constructor.
  apply logical_relation_lemma2_proj2=>// l1 l2 h12 ha1 ha2 f g
    /eval_move_stack_right h1
    /eval_move_stack_right h2.
  inv h1.
  apply valid_cut with t2; try tac_valid.
  have: entails (t ∘ l1) (t ∘ l2).
  { apply logical_relation_lemma2_proj1 with U=>//.
    by apply entails_refl. }
  apply=>//; by apply eval_move_stack_left.
Qed.

TOPLAS page 12
Definition meet r s t :=
  forall fr fs ft,
    eval r [::] fr ->
    eval s [::] fs ->
    eval t [::] ft ->
  fr ⟛ fs ++ ft.

Definition MEET U := logrel3 meet U.

Lemma c1a r s t U :
  closed r -> [ ⊢ r :- U ] ->
  closed s -> [ ⊢ s :- U ] ->
  closed t -> [ ⊢ t :- U ] ->
  box_rel3 meet r s t ->
  EQU U (neu s) (neu t).
Proof.
  have: forall r s t, box_rel3 meet r s t ->
    box_rel2 entails (neu s) (neu t) /\ box_rel2 entails (neu t) (neu s).
  { move=> {}r {}s {}t.
    elim=>{r s t}//=.
    - move=> r s t V hcr htr hcs hts hct htt h.
      have [h1 h2] := logrel3_andl_ren h.
      split; apply box_rel2_box with V;
        by [apply closed_sneu|apply has_type_neu|].
    - move=> > _ [??].
      by split; constructor.
    - move=> > _ [??].
      by split; constructor.
    - move=> > _ [??].
      by split; constructor.
    - move=> > _ [??].
      by split; constructor.
    - move=> > _ [??].
      by split; constructor.
    - move=> > _ [??].
      by split; constructor.
    - move=> x.
      by split; constructor.
    - by split; constructor.
    - by split; constructor.
    - by split; constructor.
    - by split; constructor.
    - move=> > _ [??] _ [??].
      by split; constructor.
    - move=> > _ [??] _ [??].
      by split; constructor. }
  move=> h hcr htr hcs hts hct htt /h [h1 h2].
  by split; apply b1=>//; by [apply closed_sneu|apply has_type_neu].
Qed.

Lemma c1 r s t U :
  closed r -> [ ⊢ r :- U ] ->
  closed s -> [ ⊢ s :- U ] ->
  closed t -> [ ⊢ t :- U ] ->
  box_rel3 meet r s t ->
  MEET U r s t.
Proof.
  (* We prove this lemma by induction over the weight r. *)
  have:
    forall n r s t U,
    weight r <= n ->
    closed r -> [ ⊢ r :- U ] ->
    closed s -> [ ⊢ s :- U ] ->
    closed t -> [ ⊢ t :- U ] ->
    box_rel3 meet r s t ->
    MEET U r s t.
  (* The latter generalization subsumes the lemma. *)
  2: { move=> h *. by apply (h (weight r)). }
  clear r s t U.
  elim=>[r s t U hw|n ih].
  (* case {0} *)
  { exfalso. have := weight_pos r. by lia. }
  (* case {n.+1} *)
  { case.
    (* case {Var _} *)
    { by move=> >? /closed_ids. }
    (* case {Zero} *)
    { move=> s t U /= _ _ hty hcs hts hct htt hb.
      have hU: U = Void by inv hty.
      rewrite hU in hty hts htt *.
      split; first by apply EQU_Void_neu.
      inv hb=> fr fs ft h1 h2 h3; inv h1; inv h2; inv h3.
      - split.
        + by apply valid_contradiction.
        + by apply valid_weak, valid_contradiction.
      - split.
        + by apply valid_contradiction.
        + by apply valid_weak, valid_contradiction.
      - split.
        + by apply valid_contradiction.
        + by apply valid_and_l_sym, valid_weak, valid_contradiction. }
    (* case {Top} *)
    { move=> s t U /= _ _ hty hcs hts hct htt hb.
      have hU: U = Void by inv hty.
      rewrite hU in hty hts htt *.
      split; first by apply EQU_Void_neu.
      inv hb=> fr fs ft h1 h2 h3; inv h1; inv h2; inv h3.
      by apply valid_dup. }
    (* case {And} *)
    { move=> r1 r2 s t U /= hw hcr hty1 hcs hty2 hct hty3 hb.
      inv hb.
      have[hc1 hc2]: closed r1 /\ closed r2 by apply closed_and.
      have[hc3 hc4]: closed s1 /\ closed s2 by apply closed_and.
      have[hc5 hc6]: closed t1 /\ closed t2 by apply closed_and.
      have[ht1 ht2]: [ ⊢ r1 :- U ] /\ [ ⊢ r2 :- U ] by inv hty1.
      have[ht3 ht4]: [ ⊢ s1 :- U ] /\ [ ⊢ s2 :- U ] by inv hty2.
      have[ht5 ht6]: [ ⊢ t1 :- U ] /\ [ ⊢ t2 :- U ] by inv hty3.
      have ih1: MEET U r1 s1 t1 by apply ih=>//; lia.
      have ih2: MEET U r2 s2 t2 by apply ih=>//; lia.
      apply logical_relation_lemma3_proj2=>//.
      { have[??]:= logrel3_andl ih1.
        have[??]:= logrel3_andl ih2.
        by split; apply ENT_and. }
      move=> l1 l2 l3 h123 ha1 ha2 ha3.
      have hm1: meet (r1 ∘ l1) (s1 ∘ l2) (t1 ∘ l3)
        by apply: (logical_relation_lemma3_proj1 ih1).
      have hm2: meet (r2 ∘ l1) (s2 ∘ l2) (t2 ∘ l3)
        by apply: (logical_relation_lemma3_proj1 ih2).
      move=> f1 f2 f3
        /eval_move_stack_right h1 /eval_move_stack_right h2 /eval_move_stack_right h3.
      inv h1. inv h2. inv h3.
      have[ih11 ih12]: s3 ⟛ s4 ++ s5 by apply hm1; apply eval_move_stack_left.
      have[ih21 ih22]: t3 ⟛ t4 ++ t5 by apply hm2; apply eval_move_stack_left.
      split.
      + apply valid_and_mix_r.
        by apply valid_and_and_intro.
      + apply valid_and_mix_l.
        by apply valid_and_and_intro. }
    (* case {App} *)
    { move=> r1 r2 s t V /= hw hcr hty1 hcs hty2 hct hty3 hb.
      inv hb.
      have[hc1 hc2]: closed r1 /\ closed r2 by apply closed_app.
      have[hc3 hc4]: closed s1 /\ closed s2 by apply closed_app.
      have[hc5 hc6]: closed t1 /\ closed t2 by apply closed_app.
      inv hty1.
      inv hty2.
      inv hty3.
      have e1: U = U0.
      { apply box_rel3_type_det12 with
          (R:=meet) (r:=r2) (s:=s2) (t:=t2) (Γ:=empty_ctx) (a:=0) (b:=0)=>//. }
      have e2: U = U1.
      { apply box_rel3_type_det13 with
          (R:=meet) (r:=r2) (s:=s2) (t:=t2) (Γ:=empty_ctx) (a:=0) (b:=0)=>//. }
      subst U0 U1.
      have h: MEET (Arr U V) r1 s1 t1 by apply ih=>//; lia.
      apply h=>// ξ.
      have ?: closed r2.|[ren ξ] by apply closed_unaffectedh.
      have ?: closed s2.|[ren ξ] by apply closed_unaffectedh.
      have ?: closed t2.|[ren ξ] by apply closed_unaffectedh.
      have ?: [ ⊢ r2.|[ren ξ] :- U ] by apply has_type_hsubst_0.
      have ?: [ ⊢ s2.|[ren ξ] :- U ] by apply has_type_hsubst_0.
      have ?: [ ⊢ t2.|[ren ξ] :- U ] by apply has_type_hsubst_0.
      have hbξ: box_rel3 meet r2.|[ren ξ] s2.|[ren ξ] t2.|[ren ξ]
        by apply box_rel3_preserved_ren.
      have e: weight r2.|[ren ξ] = weight r2 by apply weight_hsubst.
      split.
      - apply ih=>//.
        by lia.
      - apply ih=>//.
        + have hwn: weight (neu r2.|[ren ξ]) <= weight r2.|[ren ξ] by apply weight_neu.
          by lia.
        + by apply closed_sneu.
        + by apply has_type_neu.
        + by apply closed_sneu.
        + by apply has_type_neu.
        + by apply closed_sneu.
        + by apply has_type_neu.
        + by apply box_rel3_preserved_neu. }
    (* case {TApp} *)
    { move=> r S s t V /= hw hcr hty1 hcs hty2 hct hty3 hb.
      inv hb.
      have ?:= proj1 (closed_tapp r S) hcr.
      have ?:= proj1 (closed_tapp s0 S) hcs.
      have ?:= proj1 (closed_tapp t0 S) hct.
      inv hty1.
      inv hty2.
      inv hty3.
      have h: MEET (TArr V) r s0 t0 by apply ih.
      by apply h. }
    (* case {Lam} *)
    { move=> u U v w W hw hc1 hty1 hc2 hty2 hc3 hty3 hb.
      inv hb. inv hty1. inv hty2. inv hty3.
      have ht1: [ ⊢ Lam u U :- Arr U V ] by constructor.
      have ht2: [ ⊢ Lam s U :- Arr U V ] by constructor.
      have ht3: [ ⊢ Lam t U :- Arr U V ] by constructor.
      apply logical_relation_lemma3_proj2=>//.
      { apply c1a with (Lam u U)=>//. by constructor. }
      move=> l1 l2 l3 h123 ha1 ha2 ha3.
      inv h123.
      move: ha1 ha2 ha3=> [hcl1 hsl1] [hcl2 hsl2] [hcl3 hsl3].
      inv hcl1.
      inv hsl1.
      inv hcl2.
      inv hsl2.
      inv hcl3.
      inv hsl3.
      move=> f1 f2 f3 /eval_move_stack_right hf1
                      /eval_move_stack_right hf2
                      /eval_move_stack_right hf3.
      inv hf1.
      inv hf2.
      inv hf3.
      have hcu: closed u.[Box r/] by apply fv1; [apply closed_lam in hc1|apply closed_box].
      have hcs: closed s.[Box s0/] by apply fv1; [apply closed_lam in hc2|apply closed_box].
      have hct: closed t.[Box t0/] by apply fv1; [apply closed_lam in hc3|apply closed_box].
      have hut: [ ⊢ u.[Box r/] :- V ].
      { apply has_type_beta with U=>//; by [apply closed_box|constructor]. }
      have hst: [ ⊢ s.[Box s0/] :- V ].
      { apply has_type_beta with U=>//; by [apply closed_box|constructor]. }
      have htt: [ ⊢ t.[Box t0/] :- V ].
      { apply has_type_beta with U=>//; by [apply closed_box|constructor]. }
      have hb': box_rel3 meet u.[Box r/] s.[Box s0/] t.[Box t0/]
        by apply box_rel3_preserved_subst0 with U.
      have hw2: weight u.[Box r/] <= n.
      { have e := weight_subst_box 0 u r.
        rewrite upn0 in e.
        rewrite -e.
        simpl in hw.
        by lia. }
      have {}ih := ih _ _ _ V hw2 hcu hut hcs hst hct htt hb'.
      have hm: meet (u.[Box r/] ∘ l0) (s.[Box s0/] ∘ l4) (t.[Box t0/] ∘ l5).
      { apply: (logical_relation_lemma3_proj1 ih (l1:=l0) (l2:=l4) (l3:=l5))=>//; by split. }
      apply hm; by apply eval_move_stack_left. }
    (* case {Imp} *)
    { move=> r f s t U /= hw hcr hty1 hcs hty2 hct hty3 hb.
      inv hb.
      have ?:= proj1 (closed_imp r f) hcr.
      have ?:= proj1 (closed_imp s0 f) hcs.
      have ?:= proj1 (closed_imp t0 f) hct.
      have hU: U = Void by inv hty1.
      rewrite hU in hty1 hty2 hty3 *.
      have[??]: [ ⊢ r :- Void ] /\ [ ⊢ s0 :- Void ] by split; [inv hty1|inv hty2].
      have ?: [ ⊢ t0 :- Void ] by inv hty3.
      have h: MEET Void r s0 t0 by apply ih.
      split.
      - have[[h1 h2] _] := h.
        split=> ?? hf hg; inv hf; inv hg.
        + apply valid_imp_imp_split.
          by apply h1.
        + apply valid_imp_imp_split.
          by apply h2.
      - move=> f1 f2 f3 h1 h2 h3.
        inv h1. inv h2. inv h3.
        have[_ {}h] := h.
        have[??]: s2 ⟛ s3 ++ s4 by apply h.
        split.
        + by apply valid_and_imp3_r.
        + by apply valid_and_imp3_l. }
    (* case {TLam} *)
    { move=> r s t V /= hw hcr hty1 hcs hty2 hct hty3 hb.
      inv hb.
      apply logical_relation_lemma3_proj2=>//.
      { apply c1a with (TLam r)=>//.
        by constructor. }
      inv hty1.
      inv hty2.
      inv hty3.
      move=> l1 l2 l3 h123 ha1 ha2 ha3 /=.
      inv h123.
      move: ha1 ha2 ha3=> [hcl1 hsl1] [hcl2 hsl2] [hcl3 hsl3].
      inv hcl1.
      inv hsl1.
      inv hcl2.
      inv hsl2.
      inv hcl3.
      inv hsl3.
      move=> f1 f2 f3 /eval_move_stack_right hf1
                      /eval_move_stack_right hf2
                      /eval_move_stack_right hf3.
      inv hf1.
      inv hf2.
      inv hf3.
      have ?: closed r.|[t/] by apply closed_unaffectedh, closed_tlam.
      have ?: closed s0.|[t/] by apply closed_unaffectedh, closed_tlam.
      have ?: closed t0.|[t/] by apply closed_unaffectedh, closed_tlam.
      have ?: [ ⊢ r.|[t/] :- U ] by apply has_type_hsubst1.
      have ?: [ ⊢ s0.|[t/] :- U ] by apply has_type_hsubst1.
      have ?: [ ⊢ t0.|[t/] :- U ] by apply has_type_hsubst1.
      have hb': box_rel3 meet r.|[t/] s0.|[t/] t0.|[t/]
        by apply box_rel3_preserved_hsubst0 with empty_ctx U U U 1 1.
      have hw2: weight r.|[t/] <= n by rewrite weight_hsubst.
      have {}ih: MEET U r.|[t/] s0.|[t/] t0.|[t/] by apply ih.
      have hm: meet (r.|[t/] ∘ l0) (s0.|[t/] ∘ l4) (t0.|[t/] ∘ l5).
      { apply: (logical_relation_lemma3_proj1 ih (l1:=l0) (l2:=l4) (l3:=l5))=>//; by split. }
      apply hm; by apply eval_move_stack_left. }
    (* case {TAll} *)
    { move=> r s t V /= hw hcr hty1 hcs hty2 hct hty3 hb.
      inv hb.
      have hU: V = Void by inv hty1.
      rewrite hU in hty1 hty2 hty3 *.
      have ?:= proj1 (closed_tall r) hcr.
      have ?:= proj1 (closed_tall s0) hcs.
      have ?:= proj1 (closed_tall t0) hct.
      have ?: [ ⊢ r :- Void ] by apply has_type_lower_1; inv hty1.
      have ?: [ ⊢ s0 :- Void ] by apply has_type_lower_1; inv hty2.
      have ?: [ ⊢ t0 :- Void ] by apply has_type_lower_1; inv hty3.
      have h: MEET Void r s0 t0 by apply ih.
      split; first by apply EQU_Void_neu.
      move=> f1 f2 f3 h1 h2 h3.
      inv h1.
      inv h2.
      inv h3.
      have[_ {}h] := h.
      have[h1 h2]: s2 ⟛ s3 ++ s4 by apply h.
      have[a1 a2] := valid_all_and s3 s4.
      split.
      + apply valid_cut with (FAll (s3 ++ s4))=>//.
        by apply valid_all_mono.
      + apply valid_cut with (FAll (s3 ++ s4))=>//.
        by apply valid_all_mono. }
    (* case {Neu} *)
    { move=> r s t U /= hw hcr hty1 hcs hty2 hct hty3 hb.
      inv hb.
      have ?:= proj1 (closed_neu r) hcr.
      have ?:= proj1 (closed_neu s0) hcs.
      have ?:= proj1 (closed_neu t0) hct.
      have ?: [ ⊢ r :- U ] by inv hty1.
      have ?: [ ⊢ s0 :- U ] by inv hty2.
      have ?: [ ⊢ t0 :- U ] by inv hty3.
      have ?: closed (neu r) by apply closed_sneu.
      have ?: closed (neu s0) by apply closed_sneu.
      have ?: closed (neu t0) by apply closed_sneu.
      have ?: [ ⊢ neu r :- U ] by apply has_type_neu.
      have ?: [ ⊢ neu s0 :- U ] by apply has_type_neu.
      have ?: [ ⊢ neu t0 :- U ] by apply has_type_neu.
      have {}ih: MEET U (neu r) (neu s0) (neu t0).
      { apply ih=>//.
        - have:= weight_neu r.
          by lia.
        - by apply box_rel3_preserved_neu. }
      apply logical_relation_lemma3_proj2=>//.
      { apply logrel3_andl in ih.
        rewrite !neu_idempotent in ih.
        have[ih1 ih2] := ih.
        have ?: closed (Neu (neu s0)) by apply closed_neu.
        have ?: closed (Neu (neu t0)) by apply closed_neu.
        have ?: [ ⊢ Neu (neu s0) :- U ] by constructor.
        have ?: [ ⊢ Neu (neu t0) :- U ] by constructor.
        split=>/=.
        + apply logical_relation_lemma2_proj2=>// l1 l2 h12 ha1 ha2 f g
            /eval_move_stack_right hf /eval_move_stack_right hg.
          inv hf. inv hg.
          apply: (logical_relation_lemma2_proj1 ih1 (l1:=l1) (l2:=l2))=>//;
            [rewrite -(neu_idempotent s0)|rewrite -(neu_idempotent t0)];
            by apply eval_move_stack_left.
        + apply logical_relation_lemma2_proj2=>// l1 l2 h12 ha1 ha2 f g
            /eval_move_stack_right hf /eval_move_stack_right hg.
          inv hf. inv hg.
          apply: (logical_relation_lemma2_proj1 ih2 (l1:=l1) (l2:=l2))=>//;
            [rewrite -(neu_idempotent t0)|rewrite -(neu_idempotent s0)];
            by apply eval_move_stack_left. }
      move=> l1 l2 l3 h123 ha1 ha2 ha3.
      have {}ih: meet (neu r ∘ l1) (neu s0 ∘ l2) (neu t0 ∘ l3)
        by apply: (logical_relation_lemma3_proj1 ih).
      move=> f1 f2 f3 /eval_move_stack_right hf1
                      /eval_move_stack_right hf2
                      /eval_move_stack_right hf3.
      inv hf1.
      inv hf2.
      inv hf3.
      apply ih; by apply eval_move_stack_left. }
    (* case {Box} *)
    { move=> r s t U /= hw hcr hty1 hcs hty2 hct hty3 hb.
      inv hb.
      have hb': box_rel3 meet (Box r) (Box s0) (Box t0) by apply box_rel3_box with U0.
      have[V [hcr' [htr [hcs' [hts [hct' [htt hst]]]]]]] := box_rel3_box_ids hb'.
      have e: V = U.
      { inv hty1.
        by apply has_type_det with empty_ctx 0 0 r. }
      rewrite e in htr hts htt hst.
      apply logical_relation_lemma3_proj2=>//.
      { by apply c1a with (Box r). }
      move=> l1 l2 l3 h123 ha1 ha2 ha3.
      move=> f1 f2 f3 /eval_move_stack_right hf1
                      /eval_move_stack_right hf2
                      /eval_move_stack_right hf3.
      inv hf1.
      inv hf2.
      inv hf3.
      have h:= (logical_relation_lemma3_proj1 (proj1 hst)) l1 l2 l3.
      apply h=>//; by apply eval_move_stack_left. } }
Qed.

TOPLAS: Lemma 3.7.
Lemma fusion_meet r s t U :
  closed r -> [ ⊢ r :- U ] ->
  closed s -> [ ⊢ s :- U ] ->
  closed t -> [ ⊢ t :- U ] ->
  fusion r s t ->
  MEET U r s t.
Proof.
  (* We prove this lemma by induction over the depth of r. *)
  have:
    forall n r s t U,
    depth r <= n ->
    closed r -> [ ⊢ r :- U ] ->
    closed s -> [ ⊢ s :- U ] ->
    closed t -> [ ⊢ t :- U ] ->
    fusion r s t ->
    MEET U r s t.
  (* The latter generalization subsumes the lemma. *)
  2: { move=>h *. by apply (h (depth r)). }
  clear r s t U.
  elim=>[r s t U hd|n ih].
  (* case {0} *)
  { move=> ?????? hf.
    apply c1=>//.
    apply box_rel3_nobox, mem_box_depth=>//.
    by lia. }
  (* case {n.+1} *)
  { move=> r s t U hd hcr htr hcs hts hct htt hf.
    apply c1=>//.
    apply unfold_box_rel3 with empty_ctx U 0 0=>// u v w V hdb hu hv hw ξ.
    have hcu: closed u.
    { apply directly_box_closed with r U empty_ctx 0 0=>//.
      by apply db3_proj1 with v w s t. }
    have hcv: closed v.
    { apply directly_box_closed with s U empty_ctx 0 0=>//.
      by apply db3_proj2 with u w r t. }
    have hcw: closed w.
    { apply directly_box_closed with t U empty_ctx 0 0=>//.
      by apply db3_proj3 with u v r s. }
    have hdu: depth u <= n.
    { apply directly_box_depth with r=>//.
      by apply db3_proj1 with v w s t. }
    have hfu: fusion u v w by apply fusion_db3_fusion with r s t.
    split.
    - apply ih=>//.
      + by rewrite depth_hsubst.
      + by apply closed_unaffectedh.
      + by apply has_type_hsubst_0.
      + by apply closed_unaffectedh.
      + by apply has_type_hsubst_0.
      + by apply closed_unaffectedh.
      + by apply has_type_hsubst_0.
      + by apply fusion_preserved_hsubst.
    - apply ih=>//.
      + by rewrite -depth_neu depth_hsubst.
      + apply closed_sneu.
        by apply closed_unaffectedh.
      + apply has_type_neu.
        by apply has_type_hsubst_0.
      + apply closed_sneu.
        by apply closed_unaffectedh.
      + apply has_type_neu.
        by apply has_type_hsubst_0.
      + apply closed_sneu.
        by apply closed_unaffectedh.
      + apply has_type_neu.
        by apply has_type_hsubst_0.
      + apply fusion_preserved_neu.
        by apply fusion_preserved_hsubst. }
Qed.

Inductive all3 P : stack -> stack -> stack -> Prop :=
| all3_nil :
    all3 P [::] [::] [::]
| all3_cons_r r1 l1 r2 l2 r3 l3 :
    P r1 r2 r3 ->
    all3 P l1 l2 l3 ->
    all3 P (R r1 :: l1) (R r2 :: l2) (R r3 :: l3)
| all3_cons_t t l1 l2 l3 :
    all3 P l1 l2 l3 ->
    all3 P (T t :: l1) (T t :: l2) (T t :: l3).

Lemma all3_fusion_refl_neu l :
  all3 fusion l l (neu_stack l).
Proof.
  elim: l=>/=.
  - constructor.
  - move=> []a l h; constructor=>//.
    by apply fusion_refl_neu.
Qed.

Lemma fusion_allp_split r1 r2 r3 l1 l2 l3 :
  fusion r1 r2 r3 ->
  all3 fusion l1 l2 l3 ->
  fusion (r1 ∘ l1) (r2 ∘ l2) (r3 ∘ l3).
Proof.
  elim: l1 r1 r2 r3 l2 l3.
  - move=> r1 r2 r3 l2 l3 h1 h2.
    by inv h2=>/=.
  - move=> []a l h r1 r2 r3 l2 l3 h1 h2; inv h2=>/=.
    + apply h=>//.
      by constructor.
    + apply h=>//.
      by constructor.
Qed.

Lemma fusion_cross_neu r l :
  fusion (r ∘ l) (neu r ∘ l) (r ∘ neu_stack l).
Proof.
  elim: l r=>//=.
  - move=> >. by apply fusion_swap, fusion_refl_neu.
  - move=> []a l ih r /=.
    by apply ih.
    have?: fusion (App r a) (App (neu r) a) (App r (neu a)).
    { constructor. by apply fusion_swap, fusion_refl_neu.
                   by apply fusion_refl_neu. }
    have?:= all3_fusion_refl_neu l.
    by apply fusion_allp_split.
Qed.

TOPLAS: Corollary 3.8.
Corollary cross_lemma r l :
  complete (r ∘ l) ->
  forall f1 f2 f3,
    eval (r ∘ l) [::] f1 ->
    eval (neu r ∘ l) [::] f2 ->
    eval (r ∘ neu_stack l) [::] f3 ->
  f1 ⟛ f2 ++ f3.
Proof.
  move=> [hc ht] f1 f2 f3 h1 h2 h3.
  have?: [ ⊢ neu r ∘ l :- Void ] by apply has_type_appl_neu_head.
  have?: [ ⊢ r ∘ neu_stack l :- Void ] by apply has_type_appl_neu_stack.
  have?: closed (neu r ∘ l) by apply closed_appl_neu_head.
  have?: closed ( r ∘ neu_stack l) by apply closed_appl_neu_stack.
  have[]//:= @fusion_meet (r ∘ l) (neu r ∘ l) (r ∘ neu_stack l) Void.
    by apply fusion_cross_neu.
  move=> ?.
  by apply.
Qed.

Corollary meet_refl r U :
  closed r ->
  [ ⊢ r :- U ] ->
  MEET U r r r.
Proof.
  move=> ??.
  have?:= fusion_refl r.
  by apply fusion_meet.
Qed.

Lemma stack_rel3_meet_refl l U :
  aligned l U ->
  stack_rel3 meet U l l l.
Proof.
  elim: U l=> [|U h1 V h2|V h1] l [hcl htl]; inv hcl; inv htl.
  - by constructor.
  - constructor; last by apply h2; split.
    move=> ξ.
    have hc: closed r.|[ren ξ] by apply closed_unaffectedh.
    have ht: [ ⊢ r.|[ren ξ] :- U ] by apply has_type_hsubst_0.
    split.
    + by apply meet_refl.
    + apply meet_refl; by [apply closed_sneu|apply has_type_neu].
  - constructor.
    by apply h1; split.
Qed.

TOPLAS: Corollary 3.9.
Corollary entails_neu r U :
  closed r ->
  [ ⊢ r :- U ] ->
  ENT U r (neu r).
Proof.
  move=> h1 h2.
  have hn1: closed (neu r) by tac_neu.
  have hn2: [ ⊢ neu r :- U ] by tac_neu.
  have hfus:= fusion_refl_neu r.
  have hm:= fusion_meet h1 h2 h1 h2 hn1 hn2 hfus.
  apply entails_36=>// l hl f g hf hg.
  have h112:= stack_rel3_meet_refl hl.
  have h: meet (r ∘ l) (r ∘ l) (neu r ∘ l).
    by apply (logical_relation_lemma3_proj1 hm).
  have[{}h _] := h _ _ _ hf hf hg.
  have[_ {}h] := valid_and_elim h.
  done.
Qed.

Lemma eval_compose_and l s t g h :
  eval (s ∘ l) [::] g ->
  eval (t ∘ l) [::] h ->
  eval (And s t ∘ l) [::] (g ++ h).
Proof.
  move=> /eval_move_stack_right ? /eval_move_stack_right ?.
  apply eval_move_stack_left.
  by constructor.
Qed.

Lemma stack_rel3_meet_stack_rel2_entails U l1 l2 l3 :
  stack_rel3 meet U l1 l2 l3 ->
  stack_rel2 entails U (neu_stack l2) (neu_stack l3) /\
  stack_rel2 entails U (neu_stack l3) (neu_stack l2).
Proof.
  elim: l1 l2 l3 U.
  - move=> ??? h. inv h. split; by constructor.
  - move=> []a l1 ih l2 l3 U h; inv h => /=.
    + have[??]:= (ih _ _ _ H4).
      by split; constructor.
    + have[??]:= (ih _ _ _ H5).
      split; constructor=>// ξ; split;
        have [h20 h21]:= (H2 ξ);
        have [??] := logrel3_andl h20.
      * by rewrite -!neu_hsubst_comm.
      * by rewrite -!neu_hsubst_comm !neu_idempotent.
      * by rewrite -!neu_hsubst_comm.
      * by rewrite -!neu_hsubst_comm !neu_idempotent.
Qed.

TOPLAS Lemma 3.10. A closed recipe Φ1 is a meet of Φ2 and Φ3 if and only if Φ2♮ ≡ Φ3♮ and Φ1 ≡ Φ2 ∧ Φ3 .
Lemma l_3_10 r s t U :
  closed r -> [ ⊢ r :- U ] ->
  closed s -> [ ⊢ s :- U ] ->
  closed t -> [ ⊢ t :- U ] ->
  MEET U r s t <->
  (EQU U (neu s) (neu t) /\
   EQU U r (And s t)).
Proof.
  move=> hr1 hr2 hs1 hs2 ht1 ht2.
  split=> [h|[h1 [h2 h3]]].
  (* necessity *)
  { htac_neu U r, s, t.
    have?: closed (And s t) by apply closed_and.
    have?: [ ⊢ And s t :- U ] by constructor.
    split.
    - by have[h1 h2]:= logrel3_andl h.
    - split; apply entails_36=>// l hl.
      + have hl1:= stack_rel3_meet_refl hl.
        have {}h: meet (r ∘ l) (s ∘ l) (t ∘ l)
          by apply (logical_relation_lemma3_proj1 h).
        move=> f g hf /eval_move_stack_right hg.
        inv hg.
        apply h=>//; by apply eval_move_stack_left.
      + have hl1:= stack_rel3_meet_refl hl.
        have {}h: meet (r ∘ l) (s ∘ l) (t ∘ l)
          by apply (logical_relation_lemma3_proj1 h).
        move=> f g /eval_move_stack_right hf hg.
        inv hf.
        apply h=>//; by apply eval_move_stack_left. }
  { apply logical_relation_lemma3=>//.
    split=>//.
    have hr: MEET U r r r by apply meet_refl.
    move=> l1 l2 l3 h123 ha1 ha2 ha3 f1 f2 f3
           /eval_move_stack_right hf1
           /eval_move_stack_right hf2
           /eval_move_stack_right hf3.
    have h: meet (r ∘ l1) (r ∘ l2) (r ∘ l3) by apply (logical_relation_lemma3_proj1 hr).
    have c1: complete (r ∘ l1) by apply aligned_complete with U.
    have c2: complete (r ∘ l2) by apply aligned_complete with U.
    have c3: complete (r ∘ l3) by apply aligned_complete with U.
    have c4: complete (s ∘ l2) by apply aligned_complete with U.
    have c5: complete (s ∘ l3) by apply aligned_complete with U.
    have c6: complete ((neu s) ∘ l2) by apply aligned_complete with U=>//; tac_neu.
    have c7: complete ((neu s) ∘ l3) by apply aligned_complete with U=>//; tac_neu.
    have c8: complete (s ∘ neu_stack l2). apply aligned_complete with U=>//. by apply aligned_neu.
    have c9: complete (s ∘ neu_stack l3). apply aligned_complete with U=>//. by apply aligned_neu.
    have c10: complete (t ∘ l2) by apply aligned_complete with U.
    have c11: complete (t ∘ l3) by apply aligned_complete with U.
    have c12: complete ((neu t) ∘ l2) by apply aligned_complete with U=>//; tac_neu.
    have c13: complete ((neu t) ∘ l3) by apply aligned_complete with U=>//; tac_neu.
    have c14: complete (t ∘ neu_stack l2). apply aligned_complete with U=>//. by apply aligned_neu.
    have c15: complete (t ∘ neu_stack l3). apply aligned_complete with U=>//. by apply aligned_neu.
    have[g1 {}c1 ] := eval_def c1.
    have[g2 {}c2 ] := eval_def c2.
    have[g3 {}c3 ] := eval_def c3.
    have[g4 {}c4 ] := eval_def c4.
    have[g5 {}c5 ] := eval_def c5.
    have[g6 {}c6 ] := eval_def c6.
    have[g7 {}c7 ] := eval_def c7.
    have[g8 {}c8 ] := eval_def c8.
    have[g9 {}c9 ] := eval_def c9.
    have[g10 {}c10] := eval_def c10.
    have[g11 {}c11] := eval_def c11.
    have[g12 {}c12] := eval_def c12.
    have[g13 {}c13] := eval_def c13.
    have[g14 {}c14] := eval_def c14.
    have[g15 {}c15] := eval_def c15.

    have h4: entails (And s t ∘ l2) (r ∘ l2).
    { apply (logical_relation_lemma2_proj1 h3)=>//.
      by apply closed_and.
      by constructor.
      by apply stack_rel_entails_refl2. }
    have h5: entails (r ∘ l2) (And s t ∘ l2).
    { apply (logical_relation_lemma2_proj1 h2)=>//.
      by apply closed_and.
      by constructor.
      by apply stack_rel_entails_refl2. }
    have h6: entails (And s t ∘ l3) (r ∘ l3).
    { apply (logical_relation_lemma2_proj1 h3)=>//.
      by apply closed_and.
      by constructor.
      by apply stack_rel_entails_refl2. }
    have h7: entails (r ∘ l3) (And s t ∘ l3).
    { apply (logical_relation_lemma2_proj1 h2)=>//.
      by apply closed_and.
      by constructor.
      by apply stack_rel_entails_refl2. }

    have step0: f1 ⟛ g2 ++ g3.
    { apply eval_move_stack_left in hf1.
      by apply h. }

    have ?: g2 ⟛ g4 ++ g10.
    { have ?: eval (And s t ∘ l2) [::] (g4 ++ g10) by apply eval_compose_and.
      split.
      - by apply h5.
      - by apply h4. }
    have ?: g3 ⟛ g5 ++ g11.
    { have ?: eval (And s t ∘ l3) [::] (g5 ++ g11) by apply eval_compose_and.
      split.
      - by apply h7.
      - by apply h6. }

    have step1: f1 ⟛ (g4 ++ g10 ++ g5 ++ g11).
    { have[??]:= step0.
      unpack.
      split; apply valid_cut with (g2 ++ g3)=>//.
      - repeat apply valid_and_intro.
        + apply valid_and_l_sym, valid_weak.
          tac_valid_cut (g4 ++ g10).
        + apply valid_and_l_sym, valid_weak.
          tac_valid_cut (g4 ++ g10).
        + apply valid_weak.
          tac_valid_cut (g5 ++ g11).
        + apply valid_weak.
          tac_valid_cut (g5 ++ g11).
      - apply valid_and_intro.
        + apply valid_cut with (g4 ++ g10)=>//.
          apply valid_and_and_intro; tac_valid.
        + tac_valid_cut (g5 ++ g11). }

    have step2: f1 ⟛ (g6 ++ g8 ++ g12 ++ g14 ++ g7 ++ g9 ++ g13 ++ g15).
    { have?: g4 ⟛ g6 ++ g8.
      { apply cross_lemma with s l2=>//. by apply aligned_complete with U. }
      have?: g10 ⟛ g12 ++ g14.
      { apply cross_lemma with t l2=>//. by apply aligned_complete with U. }
      have?: g5 ⟛ g7 ++ g9.
      { apply cross_lemma with s l3=>//. by apply aligned_complete with U. }
      have?: g11 ⟛ g13 ++ g15.
      { apply cross_lemma with t l3=>//. by apply aligned_complete with U. }

      Local Ltac _local a b c :=
        apply valid_cut with a;
          [ by tac_valid
          | apply valid_cut with (b ++ c); by tac_valid].

      apply valid_equiv_cut with (g4 ++ g10 ++ g5 ++ g11).
        by apply valid_equiv_sym.
      split; repeat apply valid_and_intro; unpack;
        try by first [
          _local g4 g6 g8
        | _local g10 g12 g14
        | _local g5 g7 g9
        | _local g11 g13 g15 ].
      - apply valid_cut with (g6 ++ g8)=>//;
        apply valid_and_and_intro; tac_valid.
      - apply valid_cut with (g12 ++ g14)=>//.
        do 2 apply valid_weak.
        apply valid_and_and_intro; tac_valid.
      - apply valid_cut with (g7 ++ g9)=>//.
        do 4 apply valid_weak.
        apply valid_and_and_intro; tac_valid.
      - apply valid_cut with (g13 ++ g15)=>//.
        do 6 apply valid_weak.
        apply valid_and_and_intro; tac_valid. }

    have step3: f1 ⟛ (g6 ++ g8 ++ g6 ++ g15 ++ g13 ++ g8 ++ g13 ++ g15).
    { destruct step2 as [step2l step2r].
      split.
      - repeat match goal with
          | h: (f1 ||- _) |- _ =>
          have[? {}h] := valid_and_elim h
        end.
        by repeat apply valid_and_intro.
      - apply valid_cut with (g6 ++ g8 ++ g12 ++ g14 ++ g7 ++ g9 ++ g13 ++ g15)=>//.
        repeat (apply valid_and_and_intro; try tac_valid).
        + have: entails (neu s ∘ l2) (neu t ∘ l2).
          { have[{}h1 ?]:= h1.
            htac_neu U s, t.
            apply (logical_relation_lemma2_proj1 h1)=>//.
            by apply stack_rel_entails_refl2. }
          by apply.
        + have: entails (t ∘ neu_stack l3) (t ∘ neu_stack l2).
          { have : ENT U t t by apply entails_refl.
            move/logical_relation_lemma2_proj1.
            apply=>//; try by apply aligned_neu.
            by apply stack_rel3_meet_stack_rel2_entails with l1. }
          by apply.
        + have: entails (neu t ∘ l3) (neu s ∘ l3).
          { have[? {}h1]:= h1.
            htac_neu U s, t.
            apply (logical_relation_lemma2_proj1 h1)=>//.
            by apply stack_rel_entails_refl2. }
          by apply.
        + have: entails (s ∘ neu_stack l2) (s ∘ neu_stack l3).
          { have : ENT U s s by apply entails_refl.
            move/logical_relation_lemma2_proj1.
            apply=>//; try by apply aligned_neu.
            by apply stack_rel3_meet_stack_rel2_entails in h123 as []. }
          by apply. }

    have step4: f1 ⟛ (g6 ++ g8 ++ g15 ++ g13).
    { clear_except step3. move: step3=> [h1 h2]. split.
      - repeat match goal with
          | h: (f1 ||- _) |- _ =>
          have[? {}h] := valid_and_elim h
        end.
        by repeat apply valid_and_intro.
      - apply valid_cut with (g6 ++ g8 ++ g6 ++ g15 ++ g13 ++ g8 ++ g13 ++ g15)=>//.
        repeat apply valid_and_intro; tac_valid. }
    apply valid_equiv_cut with (g6 ++ g8 ++ g15 ++ g13)=>//.
    - destruct step4. by split.
    - have[??] : g6 ++ g8 ⟛ f2.
        { apply valid_equiv_sym.
          apply cross_lemma with s l2=>//.
          + by apply aligned_complete with U.
          + by apply eval_move_stack_left. }
      have[??] : g15 ++ g13 ⟛ f3.
        { have[??] : g13 ++ g15 ⟛ f3.
          { apply valid_equiv_sym.
            apply cross_lemma with t l3=>//.
            + by apply aligned_complete with U.
            + by apply eval_move_stack_left. }
          split.
          by apply valid_and_l_sym.
          apply valid_cut with (g13 ++ g15)=>//.
          tac_valid. }
      split.
      + apply valid_and_intro.
        * apply valid_cut with (g6 ++ g8)=>//.
          apply valid_and_intro.
          by apply valid_assumption_and.
          by apply valid_weak, valid_assumption_and.
        * apply valid_cut with (g15 ++ g13)=>//.
          tac_valid.
      + repeat apply valid_and_intro.
        * apply valid_and_l_sym, valid_weak.
          apply valid_cut with (g6 ++ g8)=>//.
          tac_valid.
        * apply valid_and_l_sym, valid_weak.
          apply valid_cut with (g6 ++ g8)=>//.
          tac_valid.
        * apply valid_weak.
          apply valid_cut with (g15 ++ g13)=>//.
          tac_valid.
        * apply valid_weak.
          apply valid_cut with (g15 ++ g13)=>//.
          tac_valid.
  }
Qed.

Print Assumptions l_3_10.

“surprising distributivity property”

Corollary c_3_10_1 s t U :
  closed s -> [ ⊢ s :- U ] ->
  closed t -> [ ⊢ t :- U ] ->
  EQU U (neu s) (neu t) ->
  MEET U (And s t) s t.
Proof.
  intros.
  have ?: closed (And s t) by apply closed_and.
  have ?: [ ⊢ And s t :- U ] by constructor.
  apply l_3_10=>//.
  repeat split=>//.
  by apply entails_refl.
  by apply entails_refl.
Qed.

c'est faux: contre exemple dans le papier: neu(λg.0) et neu(λg.g) appliqués à 0
Lemma EQU_neu2 s t U :
  closed s -> [ ⊢ s :- U ] ->
  closed t -> [ ⊢ t :- U ] ->
  EQU U (neu s) (neu t).
Proof.
Abort.

TODO : la phrase « the weak equivalence of Φ ♮ and Ψ ♮ is trivial. » dans le papier sous entend un peu que EQU_neu2 est vrai (alors que c'est faux) et qu'il faut en fait l'avoir en hypothèse.
Corollary c_3_10_2 s t U :
  closed s -> [ ⊢ s :- U ] ->
  closed t -> [ ⊢ t :- U ] ->
  EQU U (neu s) (neu t) ->
  MEET U (neu (And s t)) (neu s) (neu t).
Proof.
  intros.
  htac_neu U s, t.
  have ?: closed (neu (And s t)) by apply closed_and.
  have ?: [ ⊢ neu (And s t) :- U ] by constructor.
  apply l_3_10=>//.
  rewrite !neu_idempotent.
  repeat split=>//.
  by apply entails_refl.
  by apply entails_refl.
Qed.

Corollary c_3_10_2void s t :
  closed s -> [ ⊢ s :- Void ] ->
  closed t -> [ ⊢ t :- Void ] ->
  meet (neu (And s t)) (neu s) (neu t).
Proof.
  intros.
  htac_neu Void s, t.
  have ?: closed (neu (And s t)) by apply closed_and.
  have ?: [ ⊢ neu (And s t) :- Void ] by constructor.
  apply (l_3_10 (U:=Void))=>//.
  rewrite !neu_idempotent.
  split.
  - by apply EQU_Void_neu.
  - split; by apply entails_refl.
Qed.

When s and t have no free term variable, it is TOPLAS hypothesis.
Corollary c_3_10_3 r s t U V :
  closed r -> [ ⊢ r :- Arr U V ] ->
  closed s -> [ ⊢ s :- U ] ->
  closed t -> [ ⊢ t :- U ] ->
  (forall ξ, EQU U (neu s.|[ren ξ]) (neu t.|[ren ξ])) ->
  MEET V (App r (And s t)) (App r s) (App r t).
Proof.
  move=> hcr htr hcs hts hct htt he.
  have h1: MEET (Arr U V) r r r by apply meet_refl.
  apply h1=>//.
  - by apply closed_and.
  - by constructor.
  - move=> ξ /=.
    have ?: closed s.|[ren ξ] by apply closed_unaffectedh.
    have ?: closed t.|[ren ξ] by apply closed_unaffectedh.
    have ?: [ ⊢ s.|[ren ξ] :- U ] by apply has_type_hsubst_0.
    have ?: [ ⊢ t.|[ren ξ] :- U ] by apply has_type_hsubst_0.
    split.
    + by apply c_3_10_1.
    + by apply c_3_10_2.
Qed.

Corollary c_3_10_4 r s t U V :
  closed r -> [ ⊢ r :- Arr U V ] ->
  closed s -> [ ⊢ s :- U ] ->
  closed t -> [ ⊢ t :- U ] ->
  (forall ξ, EQU U (neu s.|[ren ξ]) (neu t.|[ren ξ])) ->
  EQU V (App r (And s t)) (And (App r s) (App r t)).
Proof.
  intros.
  have ?: closed (App r s) by apply closed_app.
  have ?: closed (App r t) by apply closed_app.
  have ?: closed (App r (And s t)) by apply closed_app; split=>//; apply closed_and.
  have ?: [ ⊢ App r (And s t) :- V ] by apply ty_app with U=>//; constructor.
  have ?: [ ⊢ App r s :- V ] by apply ty_app with U.
  have ?: [ ⊢ App r t :- V ] by apply ty_app with U.
  apply l_3_10=>//.
  by apply c_3_10_3 with U.
Qed.

End Sem.