+ ∀V0,V1,T1,V2,V,W0,W2,U0,U2. (
+ ∀X0:term. #X0 < #V0 + (#W0 + #U0 + 1) + 1 →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ V0 ⇒ V1 → V0 ⇒ V2 → ↑[O,1] V2 ≡ V →
+ W0 ⇒ W2 → U0 ⇒ U2 → 𝕓{Abbr} W0. U0 ⇒ T1 →
+ ∃∃X. 𝕗{Appl} V1. T1 ⇒ X & 𝕓{Abbr} W2. 𝕗{Appl} V. U2 ⇒ X.
+#V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H
+elim (IH … HV01 … HV02) -HV01 HV02 // #VV #HVV1 #HVV2
+elim (lift_total VV 0 1) #VVV #HVV
+lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV
+elim (tpr_inv_abbr1 … H) -H *
+(* case 1: bind *)
+[ -HV2 HVV2 #WW #UU #HWW0 #HUU0 #H destruct -T1;
+ elim (IH … HW02 … HWW0) -HW02 HWW0 // #W #HW2 #HWW
+ elim (IH … HU02 … HUU0) -HU02 HUU0 IH // #U #HU2 #HUU
+ @ex2_1_intro [2: @tpr_theta |1:skip |3: @tpr_bind ] /2 width=7/ (**) (* /4 width=7/ is too slow *)
+(* case 2: delta *)
+| -HV2 HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct -T1;
+ elim (IH … HW02 … HWW2) -HW02 HWW2 // #W #HW02 #HWW2
+ elim (IH … HU02 … HUU02) -HU02 HUU02 IH // #U #HU2 #HUUU2
+ elim (tpr_ps_bind … HWW2 HUUU2 … HUU2) -HUU2 HUUU2 #UUU #HUUU2 #HUUU1
+ @ex2_1_intro
+ [2: @tpr_theta
+ |1:skip
+ |3: @tpr_delta [3: @tpr_flat |1: skip ]
+ ] /2 width=14/ (**) (* /5 width=14/ is too slow *)
+(* case 3: zeta *)
+| -HW02 HVV HVVV #UU1 #HUU10 #HUUT1
+ elim (tpr_inv_lift … HU02 … HUU10) -HU02 #UU #HUU2 #HUU1
+ lapply (tw_lift … HUU10) -HUU10 #HUU10
+ elim (IH … HUUT1 … HUU1) -HUUT1 HUU1 IH // -HUU10 #U #HU2 #HUUU2
+ @ex2_1_intro
+ [2: @tpr_flat
+ |1: skip
+ |3: @tpr_zeta [2: @lift_flat |1: skip |3: @tpr_flat ]
+ ] /2 width=5/ (**) (* /5 width=5/ is too slow *)
+]
+qed.
+
+lemma tpr_conf_flat_cast:
+ ∀X2,V0,V1,T0,T1. (
+ ∀X0:term. #X0 < #V0 + # T0 + 1 →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ V0 ⇒ V1 → T0 ⇒ T1 → T0 ⇒ X2 →
+ ∃∃X. 𝕗{Cast} V1. T1 ⇒ X & X2 ⇒ X.
+#X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02
+elim (IH … HT01 … HT02) -HT01 HT02 IH /3/
+qed.
+
+lemma tpr_conf_beta_beta:
+ ∀W0:term. ∀V0,V1,T0,T1,V2,T2. (
+ ∀X0:term. #X0 < #V0 + (#W0 + #T0 + 1) + 1 →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
+ ∃∃X. 𝕓{Abbr} V1. T1 ⇒X & 𝕓{Abbr} V2. T2 ⇒ X.
+#W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
+elim (IH … HV01 … HV02) -HV01 HV02 //
+elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/
+qed.
+
+lemma tpr_conf_delta_delta:
+ ∀V0,V1,T0,T1,TT1,V2,T2,TT2. (
+ ∀X0:term. #X0 < #V0 +#T0 + 1→
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
+ ⋆. 𝕓{Abbr} V1 ⊢ T1 [O, 1] ≫ TT1 →
+ ⋆. 𝕓{Abbr} V2 ⊢ T2 [O, 1] ≫ TT2 →
+ ∃∃X. 𝕓{Abbr} V1. TT1 ⇒ X & 𝕓{Abbr} V2. TT2 ⇒ X.
+#V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2
+elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
+elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2
+elim (tpr_ps_bind … HV1 HT1 … HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1
+elim (tpr_ps_bind … HV2 HT2 … HTT2) -HT2 HTT2 #U2 #TTU2 #HTU2
+elim (ps_conf … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2
+@ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
+qed.
+
+lemma tpr_conf_delta_zeta:
+ ∀X2,V0,V1,T0,T1,TT1,T2. (
+ ∀X0:term. #X0 < #V0 +#T0 + 1→
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X