X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc_2A1%2Fllpx_sn%2Flpx_conj.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc_2A1%2Fllpx_sn%2Flpx_conj.etc;h=0000000000000000000000000000000000000000;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=5950f1b920ae26ab926c5400d19b9d3c327e1c02;hpb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/llpx_sn/lpx_conj.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/llpx_sn/lpx_conj.etc
deleted file mode 100644
index 5950f1b92..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/llpx_sn/lpx_conj.etc
+++ /dev/null
@@ -1,120 +0,0 @@
-include "basic_2/relocation/lleq_alt.ma".
-include "basic_2/reduction/cpx_lleq.ma".
-include "basic_2/reduction/lpx_lleq.ma".
-
-lemma not_ex_to_all_not: ∀A:Type[0]. ∀R:predicate A.
-                         ((∃a. R a)→⊥) → (∀a. R a → ⊥).
-/3 width=2 by ex_intro/ qed-.
-
-lemma lt_repl_sn_trans_tw: ∀L1,L2,T1,T2. ♯{L1, T1} < ♯{L2, T2} →
-                           ∀U1. ♯{U1} = ♯{T1} → ♯{L1, U1} < ♯{L2, T2}.
-normalize in ⊢ (?→?→?→?→?%%→?→?→?%%); //
-qed-.
-
-axiom cpx_fwd_lift1: ∀h,g,G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ➡[h, g] U2 →
-                     ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → ∃T2. ⇧[d, e] T2 ≡ U2.
-(*
-#h #g #G #L #U1 #U2 #H elim H -G -L -U1 -U2
-[ * #i #G #L #T1 #d #e #H
-  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=2 by ex_intro/
-  | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=2 by lift_lref_ge_minus, lift_lref_lt, ex_intro/
-  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=2 by ex_intro/
-  ]
-| #G #L #k #l #Hkl #T1 #d #e #H
-  lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3 by ex_intro/
-| #I #G #L #K #V1 #V2 #W2 #i #HLK #HV12 #HVW2 #IHV2 #T1 #d #e #H
-  elim (lift_inv_lref2 … H) -H * #Hid #H destruct
-  [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
-    elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
-    elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m /3 width=9 by cpx_delta, ex2_intro/
-  | elim (le_inv_plus_l … Hid) #Hdie #Hei
-    lapply (ldrop_conf_ge … HLK … HLV ?) -L // #HKLV
-    elim (lift_split … HVW2 d (i - e + 1)) -HVW2 /3 width=1 by le_S, le_S_S/ -Hid -Hdie
-    #V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O /3 width=9 by cpx_delta, ex2_intro/
-  ]
-| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
-  elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
-  elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=6 by cpx_bind, ldrop_skip, lift_bind, ex2_intro/
-| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
-  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHV12 … HLK … HWV1) -V1
-  elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpx_flat, lift_flat, ex2_intro/
-| #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #s #d #e #HLK #X #H
-  elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHU1 (K.ⓓW1) s … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
-  elim (lift_div_le … HU2 … HTU) -U /3 width=5 by cpx_zeta, ex2_intro/
-| #G #L #V #U1 #U2 #_ #IHU12 #K #s #d #e #HLK #X #H
-  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3 by cpx_tau, ex2_intro/
-| #G #L #V1 #V2 #U1 #_ #IHV12 #K #s #d #e #HLK #X #H
-  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHV12 … HLK … HWV1) -L -V1 /3 width=3 by cpx_ti, ex2_intro/
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
-  elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
-  elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
-  elim (IHV12 … HLK … HV01) -V1 #V3 #HV32 #HV03
-  elim (IHT12 (K.ⓛW0) s … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
-  elim (IHW12 … HLK … HW01) -W1
-  /4 width=7 by cpx_beta, lift_bind, lift_flat, ex2_intro/
-| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
-  elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
-  elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
-  elim (IHV1 … HLK … HV01) -V1 #V3 #HV3 #HV03
-  elim (IHT12 (K.ⓓW0) s … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
-  elim (IHW12 … HLK … HW01) -W1 #W3 #HW32 #HW03
-  elim (lift_trans_le … HV3 … HV2) -V
-  /4 width=9 by cpx_theta, lift_bind, lift_flat, ex2_intro/
-]
-qed-.
-*)
-lemma cpx_fwd_nlift2: ∀h,g,G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ➡[h, g] U2 → ∀d,e.
-                      (∀T2. ⇧[d, e] T2 ≡ U2 → ⊥) → (∀T1. ⇧[d, e] T1 ≡ U1 → ⊥).
-#h #g #G #L #U1 #U2 #HU12 #d #e #HnU2 #T1 #HTU1
-elim (cpx_fwd_lift1 … HU12 … HTU1) -L -U1 /2 width=2 by/
-qed-.
-
-fact lleq_lpx_cpx_trans_aux: ∀h,g,G,T1,L1s,L1d,d. L1s ⋕[T1, d] L1d →
-                             ∀Y,L2d. ⦃G, Y⦄ ⊢ ➡[h, g] L2d → Y = L1d → d = 0 →
-                             ∀T2. ⦃G, L1d⦄ ⊢ T1 ➡[h, g] T2 →
-                             ∃∃L2s. ⦃G, L1s⦄ ⊢ ➡[h, g] L2s & L2s ⋕[T2, d] L2d.
-#h #g #G #T1 #L1s @(f2_ind … rfw … L1s T1) -L1s -T1 #n #IH
-#Ys #U1 #Hn #Yd #d #HU1 elim (lleq_fwd_alt … HU1) #H #IHU1
-#Y #L2d * -Y -L2d
-[ -IH -IHU1 -HU1 #HY #Hd #U2 #HU12 destruct
-  >(length_inv_zero_dx … H) -Ys /2 width=3 by ex2_intro/
-| #Id #L1d #L2d #W1d #W2d #HL12d #HW12d #HY #Hd #U2 #HU12 destruct
-  elim (length_inv_pos_dx … H) -H #Is #L1s #W1s #_ #H destruct
-  elim (is_lift_dec U1 0 1) [ -IHU1 -HW12d | -HU1 ]
-  [ * #T1 #HTU1 lapply (lift_fwd_tw … HTU1) #H
-    lapply (lleq_inv_lift_le … HU1 L1s L1d … HTU1 ?) -HU1 /2 width=1 by ldrop_drop/
-    #HT1 elim (cpx_inv_lift1 … HU12 L1d … HTU1) -HU12 -HTU1 /2 width=4 by ldrop_drop/
-    #T2 #HTU2 #HT12 elim (IH … HT1 … HL12d … HT12) /2 width=3 by lt_repl_sn_trans_tw/ -IH -HT1 -HT12 -H
-    #L2s #HL12s #HT2 @(ex2_intro … (L2s.ⓑ{Is}W1s))
-    /3 width=10 by lleq_lift_le, lpx_pair, ldrop_drop/ (**) (* full auto too slow *)
-  | #HnU1 lapply (not_ex_to_all_not … HnU1) -HnU1 #HnU1
-    elim (IHU1 … HnU1) [2,3,4: // |5,6,7,8,9,10: skip ] -HnU1 #H1 #H2 #HW1s destruct
-    elim (IH … HW1s … HL12d … HW12d) // #L2s #HL12s #HW2d
-    @(ex2_intro … (L2s.ⓑ{Id}W2d)) /3 width=3 by lleq_cpx_trans, lpx_pair/
-    lapply (lleq_fwd_length … HW2d) #HL2sd -HW12d -HW1s
-    @lleq_intro_alt [ normalize // ] -HL2sd
-    #I2s #I2d #K2s #K2d #V2s #V2d #i @(nat_ind_plus … i) -i
-    [ #_ #_ #HLK2s #HLK2d -IH -IHU1 -HU12 -HL12s -HL12d
-      lapply (ldrop_inv_O2 … HLK2s) -HLK2s #H destruct
-      lapply (ldrop_inv_O2 … HLK2d) -HLK2d #H destruct /2 width=1 by and3_intro/
-    | #i #_ #_ #HnU2 #HLK2s #HLK2d
-      lapply (cpx_fwd_nlift2 … HU12 … HnU2) -HU12 -HnU2 #HnU1
-      lapply (ldrop_inv_drop1 … HLK2s) -HLK2s #HLK2s
-      lapply (ldrop_inv_drop1 … HLK2d) -HLK2d #HLK2d
-      elim (lpx_ldrop_trans_O1 … HL12s … HLK2s) -L2s #Y #HLK1s #H
-      elim (lpx_inv_pair2 … H) -H #K1s #V1s #HK12s #HV12s #H destruct
-      elim (lpx_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H
-      elim (lpx_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct
-      elim (IHU1 … HnU1) [2,3,4: /2 width=2 by ldrop_drop/ | 5,6,7,8,9,10: skip ] -IHU1 -HnU1 -HLK1d
-      #H1 #H2 #HV1d destruct
-      lapply (ldrop_fwd_rfw … HLK1s) -HLK1s #H
-      elim (IH … HV1d … HK12d … HV12d) // -IH -HV1d -HK12d -HV12d
-      [ #Y #H1Y #H2Y   
-       
-      
-