X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fdynamic%2Fsnv.ma;h=2be5715258a1adced3f0d0a67bda6d15e6453a0f;hb=4bea40e6589ce21c15ecf99bdd5bd2a1c62f6809;hp=2a234c2267ce4ff63fcead7177798e8e9966cd17;hpb=943bfd67310c34c05cbba627272864eb10800143;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma
index 2a234c226..2be571525 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma
@@ -26,7 +26,7 @@ inductive snv (h:sh) (g:sd h): lenv → predicate term ≝
             ⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 →
             ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T)
 | snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T →
-            ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ W ⬌* U → snv h g L (ⓝW.T)
+            ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ U ⬌* W → snv h g L (ⓝW.T)
 .
 
 interpretation "stratified native validity (term)"
@@ -85,17 +85,17 @@ lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] →
 
 fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T →
                        ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] & 
-                              L ⊢ W ⬌* U & ⦃h, L⦄ ⊢ T •[g, l + 1] U.
+                              ⦃h, L⦄ ⊢ T •[g, l + 1] U & L ⊢ U ⬌* W.
 #h #g #L #X * -L -X
 [ #L #k #W #T #H destruct
 | #I #L #K #V #i #_ #_ #W #T #H destruct
 | #a #I #L #V #T0 #_ #_ #W #T #H destruct
 | #a #L #V #W0 #W00 #T0 #U #l #_ #_ #_ #_ #_ #W #T #H destruct
-| #L #W0 #T0 #U0 #l #HW0 #HT0 #HTU0 #HWU0 #W #T #H destruct /2 width=4/
+| #L #W0 #T0 #U0 #l #HW0 #HT0 #HTU0 #HUW0 #W #T #H destruct /2 width=4/
 ]
 qed.
 
 lemma snv_inv_cast: ∀h,g,L,W,T. ⦃h, L⦄ ⊩ ⓝW.T :[g] →
-                    ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] & 
-                           L ⊢ W ⬌* U & ⦃h, L⦄ ⊢ T •[g, l + 1] U.
+                    ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] &
+                           ⦃h, L⦄ ⊢ T •[g, l + 1] U & L ⊢ U ⬌* W.
 /2 width=3/ qed-.