- we introduced the pointer_step rc in the perspective of proving

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / reducibility / ltpr_aaa.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma
index 4b716c3429c50618ed019eead964c78b1dbac507..b45dbb99eb2fe5333ed2c773f9d911ad90d5a5e7 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma
@@ -55,12 +55,12 @@ fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T
     elim (aaa_inv_abst … HT1) -HT1 #B0 #A0 #HB0 #HA0 #H destruct
     lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
     lapply (IH … HB0  … HL12 W2 ?) -HB0 /width=5/ #HB0
-    lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/
+    lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 [2,4: // |3,5: skip ] /2 width=1/ -T0 -L1 -V1 /4 width=7/
   | #a #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct
     elim (aaa_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0
     lapply (IH … HW0  … HL12 … HW02) -HW0 /width=5/ #HW2
     lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0
-    lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2
+    lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 [2,4: // |3,5: skip ] /2 width=1/ -V1 -T0 -L1 -W0 #HT2
     @(aaa_abbr … HW2) -HW2
     @(aaa_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *)
   ]