matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basic_2/substitution/cpys_cpys.ma".
  16 include "basic_2/substitution/lleq.ma".
  17
  18 (* Advanced forward lemmas **************************************************)
  19
  20 lemma lleq_fwd_lref: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
  21                      ∨∨ |L1| ≤ i ∧ |L2| ≤ i
  22                       | i < d
  23                       | ∃∃I1,I2,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V &
  24                                          ⇩[0, i] L2 ≡ K2.ⓑ{I2}V &
  25                                          K1 ⋕[V, 0] K2 & d ≤ i.
  26 #L1 #L2 #d #i * #HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=3 by or3_intro0, conj/
  27 elim (lt_or_ge i d) /2 width=1 by or3_intro1/ #Hdi #Hi
  28 elim (ldrop_O1_lt … Hi) #I1 #K1 #V1 #HLK1
  29 elim (ldrop_O1_lt L2 i) // -Hi #I2 #K2 #V2 #HLK2
  30 lapply (ldrop_fwd_length_minus2 … HLK2) #H
  31 lapply (ldrop_fwd_length_minus2 … HLK1) >HL12 <H -HL12 -H
  32 #H lapply (injective_plus_l … H) -H #HK12
  33 elim (lift_total V1 0 (i+1)) #W1 #HVW1
  34 elim (lift_total V2 0 (i+1)) #W2 #HVW2
  35 elim (IH W1) elim (IH W2) #_ #H2 #H1 #_
  36 elim (cpys_inv_lref1_ldrop … (H1 ?) … HLK2 … HVW1) -H1
  37 [ elim (cpys_inv_lref1_ldrop … (H2 ?) … HLK1 … HVW2) -H2 ]
  38 /3 width=7 by cpys_subst, yle_inj/ -W1 -W2 #H12 #_ #_ #H21 #_ #_
  39 lapply (cpys_antisym_eq … H12 … H21) -H12 -H21 #H destruct
  40 @or3_intro2 @(ex4_5_intro … HLK1 HLK2) // @conj // -HK12
  41 #V elim (lift_total V 0 (i+1))
  42 #W #HVW elim (IH W) -IH #H12 #H21 @conj #H
  43 [ elim (cpys_inv_lref1_ldrop … (H12 ?) … HLK2 … HVW) -H12 -H21
  44 | elim (cpys_inv_lref1_ldrop … (H21 ?) … HLK1 … HVW) -H21 -H12
  45 ] /3 width=7 by cpys_subst, yle_inj/
  46 qed-.