partial commit: just the components before "static" ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / ssta_ssta.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma
index 617ef508f0448f3b29d822ba72cdb028d9ef5ec8..87e0d216858dc20e80e9b1a42e25a908b062c632 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma
@@ -19,8 +19,8 @@ include "basic_2/static/ssta_lift.ma".
 (* Main properties **********************************************************)
 
 (* Note: apparently this was missing in basic_1 *)
-theorem ssta_mono: ∀h,g,L,T,U1,l1. ⦃h, L⦄ ⊢ T •[g] ⦃l1, U1⦄ →
-                   ∀U2,l2. ⦃h, L⦄ ⊢ T •[g] ⦃l2, U2⦄ → l1 = l2 ∧ U1 = U2.
+theorem ssta_mono: ∀h,g,L,T,U1,l1. ⦃G, L⦄ ⊢ T •[h, g] ⦃l1, U1⦄ →
+                   ∀U2,l2. ⦃G, L⦄ ⊢ T •[h, g] ⦃l2, U2⦄ → l1 = l2 ∧ U1 = U2.
 #h #g #L #T #U1 #l1 #H elim H -L -T -U1 -l1
 [ #L #k #l #Hkl #X #l2 #H
   elim (ssta_inv_sort1 … H) -H #Hkl2 #H destruct
@@ -49,7 +49,7 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma ssta_inv_refl_pos: ∀h,g,L,T,l. ⦃h, L⦄ ⊢ T •[g] ⦃l+1, T⦄ → ⊥.
+lemma ssta_inv_refl_pos: ∀h,g,L,T,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, T⦄ → ⊥.
 #h #g #L #T #l #HTT
 elim (ssta_fwd_correct … HTT) <minus_plus_m_m #U #HTU
 elim (ssta_mono … HTU … HTT) -h -L #H #_ -T -U