- nDestructTac: Sys.break handled in two places

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / unfold / ltpss_tpss.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma
index 0a49ef84902aebe7d7a85532ad7922babccbd761..52b52e55dc131ec241eec498f681b42aeaf56d22 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma
@@ -19,19 +19,19 @@ include "basic_2/unfold/ltpss_tps.ma".
 
 (* Properties concerning partial unfold on terms ****************************)
 
-lemma ltpss_tpss_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 →
-                          ∀L1,d1,e1. L0 [d1, e1] ▶* L1 → d1 + e1 ≤ d2 →
-                          L1 ⊢ T2 [d2, e2] ▶* U2.
+lemma ltpss_tpss_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 →
+                          ∀L1,d1,e1. L0 ▶* [d1, e1] L1 → d1 + e1 ≤ d2 →
+                          L1 ⊢ T2 ▶* [d2, e2] U2.
 #L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 //
 #U #U2 #_ #HU2 #IHU
 lapply (ltpss_tps_conf_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/
 qed.
 
 (* Basic_1: was: subst1_subst1_back *)
-lemma ltpss_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
-                      ∀L1,d1,e1. L0 [d1, e1] ▶* L1 →
-                      ∃∃T. L1 ⊢ T2 [d2, e2] ▶ T &
-                           L1 ⊢ U2 [d1, e1] ▶* T.
+lemma ltpss_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
+                      ∀L1,d1,e1. L0 ▶* [d1, e1] L1 →
+                      ∃∃T. L1 ⊢ T2 ▶ [d2, e2] T &
+                           L1 ⊢ U2 ▶* [d1, e1] T.
 #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
 [ /2 width=3/
 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01
@@ -60,19 +60,19 @@ lemma ltpss_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
 ]
 qed.
   
-lemma ltpss_tpss_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 →
-                           ∀L1,d1,e1. L1 [d1, e1] ▶* L0 → d1 + e1 ≤ d2 →
-                           L1 ⊢ T2 [d2, e2] ▶* U2.
+lemma ltpss_tpss_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 →
+                           ∀L1,d1,e1. L1 ▶* [d1, e1] L0 → d1 + e1 ≤ d2 →
+                           L1 ⊢ T2 ▶* [d2, e2] U2.
 #L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 //
 #U #U2 #_ #HU2 #IHU
 lapply (ltpss_tps_trans_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/
 qed.
 
 (* Basic_1: was: subst1_subst1 *)
-lemma ltpss_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
-                       ∀L1,d1,e1. L1 [d1, e1] ▶* L0 →
-                       ∃∃T. L1 ⊢ T2 [d2, e2] ▶ T &
-                            L0 ⊢ T [d1, e1] ▶* U2.
+lemma ltpss_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
+                       ∀L1,d1,e1. L1 ▶* [d1, e1] L0 →
+                       ∃∃T. L1 ⊢ T2 ▶ [d2, e2] T &
+                            L0 ⊢ T ▶* [d1, e1] U2.
 #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
 [ /2 width=3/
 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10