1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/substitution/cpys_cpys.ma".
16 include "basic_2/substitution/lleq.ma".
18 (* Advanced forward lemmas **************************************************)
20 lemma lleq_fwd_lref: ∀L1,L2. ∀d:ynat. ∀i:nat. L1 ⋕[#i, d] L2 →
21 ∨∨ |L1| ≤ i ∧ |L2| ≤ i
23 | ∃∃I1,I2,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V &
24 ⇩[0, i] L2 ≡ K2.ⓑ{I2}V &
25 K1 ⋕[V, yinj 0] K2 & d ≤ yinj i.
26 #L1 #L2 #d #i * #HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=3 by or3_intro0, conj/
27 elim (ylt_split 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 ] [1,3: >yminus_Y_inj ] /3 width=7 by cpys_subst_Y2, yle_inj/