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_lift.ma".
16 include "basic_2/substitution/lleq.ma".
18 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
20 (* Advanced properties ******************************************************)
22 lemma lleq_skip: ∀L1,L2,d,i. yinj i < d → |L1| = |L2| → L1 ⋕[#i, d] L2.
23 #L1 #L2 #d #i #Hid #HL12 @conj // -HL12
24 #U @conj #H elim (cpys_inv_lref1 … H) -H // *
25 #I #Z #Y #X #H elim (ylt_yle_false … Hid … H)
28 lemma lleq_lref: ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
29 ⇩[0, i] L1 ≡ K1.ⓑ{I1}V → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V →
30 K1 ⋕[V, 0] K2 → L1 ⋕[#i, d] L2.
31 #I1 #I2 #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 * #HK12 #IH @conj [ -IH | -HK12 ]
32 [ lapply (ldrop_fwd_length … HLK1) -HLK1 #H1
33 lapply (ldrop_fwd_length … HLK2) -HLK2 #H2
34 >H1 >H2 -H1 -H2 normalize //
35 | #U @conj #H elim (cpys_inv_lref1 … H) -H // *
36 >yminus_Y_inj #I #K #X #W #_ #_ #H #HVW #HWU
37 [ letin HLK ≝ HLK1 | letin HLK ≝ HLK2 ]
38 lapply (ldrop_mono … H … HLK) -H #H destruct elim (IH W)
39 /3 width=7 by cpys_subst_Y2/
43 lemma lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → L1 ⋕[#i, d] L2.
44 #L1 #L2 #d #i #HL1 #HL2 #HL12 @conj // -HL12
45 #U @conj #H elim (cpys_inv_lref1 … H) -H // *
46 #I #Z #Y #X #_ #_ #H lapply (ldrop_fwd_length_lt2 … H) -H
47 #H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/