advances on lfsx ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / llpx_sn / llpx_sn_drop.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_drop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_drop.etc
index 9bb605e39bae2cf52811f5fd70feda5b839a2f21..34980b9f61d1deb18a1df2090ccb14e3cd68d4e4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_drop.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_drop.etc
@@ -125,48 +125,6 @@ lemma llpx_sn_bind_repl_O: ∀R,I,L1,L2,V1,V2,T. llpx_sn R 0 T (L1.ⓑ{I}V1) (L2
                            ∀J,W1,W2. llpx_sn R 0 W1 L1 L2 → R L1 W1 W2 → llpx_sn R 0 T (L1.ⓑ{J}W1) (L2.ⓑ{J}W2).
 /3 width=9 by llpx_sn_bind_repl_SO, llpx_sn_inv_S/ qed-.
 
-lemma llpx_sn_dec: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
-                   ∀T,L1,L2,l. Decidable (llpx_sn R l T L1 L2).
-#R #HR #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
-#x #IH #L1 * *
-[ #s #Hx #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_sort/
-| #i #Hx #L2 elim (eq_nat_dec (|L1|) (|L2|))
-  [ #HL12 #l elim (ylt_split i l) /3 width=1 by llpx_sn_skip, or_introl/
-    #Hli elim (lt_or_ge i (|L1|)) #HiL1
-    elim (lt_or_ge i (|L2|)) #HiL2 /3 width=1 by or_introl, llpx_sn_free/
-    elim (drop_O1_lt (Ⓕ) … HiL2) #I2 #K2 #V2 #HLK2
-    elim (drop_O1_lt (Ⓕ) … HiL1) #I1 #K1 #V1 #HLK1
-    elim (eq_bind2_dec I2 I1)
-    [ #H2 elim (HR K1 V1 V2) -HR
-      [ #H3 elim (IH K1 V1 … K2 0) destruct
-        /3 width=9 by llpx_sn_lref, drop_fwd_rfw, or_introl/
-      ]
-    ]
-    -IH #H3 @or_intror
-    #H elim (llpx_sn_fwd_lref … H) -H [1,3,4,6,7,9: * ]
-    [1,3,5: /3 width=4 by lt_to_le_to_lt, lt_refl_false/
-    |7,8,9: /2 width=4 by ylt_yle_false/
-    ]
-    #Z #Y1 #Y2 #X1 #X2 #HLY1 #HLY2 #HY12 #HX12
-    lapply (drop_mono … HLY1 … HLK1) -HLY1 -HLK1
-    lapply (drop_mono … HLY2 … HLK2) -HLY2 -HLK2
-    #H #H0 destruct /2 width=1 by/
-  ]
-| #p #Hx #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_gref/
-| #a #I #V #T #Hx #L2 #l destruct
-  elim (IH L1 V … L2 l) /2 width=1 by/
-  elim (IH (L1.ⓑ{I}V) T … (L2.ⓑ{I}V) (⫯l)) -IH /3 width=1 by or_introl, llpx_sn_bind/
-  #H1 #H2 @or_intror
-  #H elim (llpx_sn_inv_bind … H) -H /2 width=1 by/
-| #I #V #T #Hx #L2 #l destruct
-  elim (IH L1 V … L2 l) /2 width=1 by/
-  elim (IH L1 T … L2 l) -IH /3 width=1 by or_introl, llpx_sn_flat/
-  #H1 #H2 @or_intror
-  #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/
-]
--x /4 width=4 by llpx_sn_fwd_length, or_intror/
-qed-.
-
 (* Inversion lemmas on negated lazy pointwise extension *********************)
 
 lemma nllpx_sn_inv_bind: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →