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. 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 … H) -H
26 /2 width=1 by ylt_inj/
29 lemma lleq_lref: ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ i →
30 ⇩[0, i] L1 ≡ K1.ⓑ{I1}V → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V →
31 K1 ⋕[V, 0] K2 → L1 ⋕[#i, d] L2.
32 #I1 #I2 #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 * #HK12 #IH @conj [ -IH | -HK12 ]
33 [ lapply (ldrop_fwd_length … HLK1) -HLK1 #H1
34 lapply (ldrop_fwd_length … HLK2) -HLK2 #H2
35 >H1 >H2 -H1 -H2 normalize //
36 | #U @conj #H elim (cpys_inv_lref1 … H) -H // *
37 #I #K #X #W #_ #_ #H #HVW #HWU
38 [ lapply (ldrop_mono … H … HLK1) | lapply (ldrop_mono … H … HLK2) ] -H
39 #H destruct elim (IH W) /3 width=7 by cpys_subst, yle_inj/
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/