]
| #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X;
+ lapply (tps_leq_repl_dx … HT02 (L. 𝕓{I} V1) ?) -HT02 /2/ #HT02
elim (IHV01 … HV02) -IHV01 HV02 #V #HV1 #HV2
elim (IHT01 … HT02) -IHT01 HT02 #T #HT1 #HT2
- lapply (tps_leq_repl … HT1 (L. 𝕓{I} V1) ?) -HT1 /2/
- lapply (tps_leq_repl … HT2 (L. 𝕓{I} V2) ?) -HT2 /3 width=5/
+ lapply (tps_leq_repl_dx … HT1 (L. 𝕓{I} V) ?) -HT1 /2/
+ lapply (tps_leq_repl_dx … HT2 (L. 𝕓{I} V) ?) -HT2 /3 width=5/
| #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X;
elim (IHV01 … HV02) -IHV01 HV02;
elim (IHV01 … HV02 H) -IHV01 HV02 #V #HV1 #HV2
elim (IHT01 … HT02 ?) -IHT01 HT02
[ -H #T #HT1 #HT2
- lapply (tps_leq_repl … HT1 (L2. 𝕓{I} V1) ?) -HT1 /2/
- lapply (tps_leq_repl … HT2 (L1. 𝕓{I} V2) ?) -HT2 /3 width=5/
+ lapply (tps_leq_repl_dx … HT1 (L2. 𝕓{I} V) ?) -HT1 /2/
+ lapply (tps_leq_repl_dx … HT2 (L1. 𝕓{I} V) ?) -HT2 /3 width=5/
| -HV1 HV2 >plus_plus_comm_23 >plus_plus_comm_23 in ⊢ (? ? %) elim H -H #H
[ @or_introl | @or_intror ] /2 by monotonic_le_plus_l/ (**) (* /3/ is too slow *)
]
<(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /4/
| #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X;
- lapply (tps_leq_repl … HT02 (L. 𝕓{I} V1) ?) -HT02 /2/ #HT02
+ lapply (tps_leq_repl_dx … HT02 (L. 𝕓{I} V0) ?) -HT02 /2/ #HT02
elim (IHV10 … HV02 ?) -IHV10 HV02 // #V
elim (IHT10 … HT02 ?) -IHT10 HT02 [2: /2/ ] #T #HT1 #HT2
- lapply (tps_leq_repl … HT2 (L. 𝕓{I} V) ?) -HT2 /3 width=6/
+ lapply (tps_leq_repl_dx … HT1 (L. 𝕓{I} V) ?) -HT1;
+ lapply (tps_leq_repl_dx … HT2 (L. 𝕓{I} V2) ?) -HT2 /3 width=6/
| #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X;
elim (IHV10 … HV02 ?) -IHV10 HV02 //
elim (IHT10 … HT02 ?) -IHT10 HT02 // /3 width=6/
]
qed.
-(*
- Theorem subst0_subst0: (t1,t2,u2:?; j:?) (subst0 j u2 t1 t2) ->
- (u1,u:?; i:?) (subst0 i u u1 u2) ->
- (EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t t2)).
-
- Theorem subst0_subst0_back: (t1,t2,u2:?; j:?) (subst0 j u2 t1 t2) ->
- (u1,u:?; i:?) (subst0 i u u2 u1) ->
- (EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t2 t)).
-
-*)