- basic_2: induction for preservation results now uses supclosure

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / fsup.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
index 6b0ee2185bd01f8728e12fdeeb69da44021c8d58..cffa08c68bc0b4c6909508d3b62b9ae4973c966e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
@@ -18,9 +18,8 @@ include "basic_2/relocation/ldrop.ma".
 
 inductive fsup: bi_relation lenv term ≝
 | fsup_lref   : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V
-| fsup_bind_sn: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) L V
+| fsup_pair_sn: ∀I,L,V,T. fsup L (②{I}V.T) L V
 | fsup_bind_dx: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
-| fsup_flat_sn: ∀I,L,V,T.   fsup L (ⓕ{I}V.T) L V
 | fsup_flat_dx: ∀I,L,V,T.   fsup L (ⓕ{I}V.T) L T
 | fsup_ldrop  : ∀L1,K1,K2,T1,T2,U1,d,e.
                 ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 →
@@ -57,11 +56,11 @@ qed-.
 
 fact fsup_fwd_length_lref1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀i. T1 = #i → |L2| < |L1|.
 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2
-[ 6: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct
-     lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
-     elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct
-     @(lt_to_le_to_lt … HLK1) /2 width=2/
-| normalize // |2,3: #a
+[5: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct
+    lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
+    elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct
+    @(lt_to_le_to_lt … HLK1) /2 width=2/
+| normalize // |3: #a
 ] #I #L #V #T #j #H destruct
 qed-.