∃∃K2. K1 ≃[0, ⫰e] K2 & L2 = K2.ⓑ{I}V.
/2 width=6 by leq_inv_pair1_aux/ qed-.
+lemma leq_inv_pair: ∀I1,I2,L1,L2,V1,V2,e. L1.ⓑ{I1}V1 ≃[0, e] L2.ⓑ{I2}V2 → 0 < e →
+ ∧∧ L1 ≃[0, ⫰e] L2 & I1 = I2 & V1 = V2.
+#I1 #I2 #L1 #L2 #V1 #V2 #e #H #He elim (leq_inv_pair1 … H) -H //
+#Y #HL12 #H destruct /2 width=1 by and3_intro/
+qed-.
+
fact leq_inv_succ1_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → 0 < d →
∃∃J2,K2,W2. K1 ≃[⫰d, e] K2 & L2 = K2.ⓑ{J2}W2.
/3 width=3 by leq_inv_atom1, leq_sym/
qed-.
+lemma leq_inv_succ: ∀I1,I2,L1,L2,V1,V2,d,e. L1.ⓑ{I1}V1 ≃[d, e] L2.ⓑ{I2}V2 → 0 < d →
+ L1 ≃[⫰d, e] L2.
+#I1 #I2 #L1 #L2 #V1 #V2 #d #e #H #Hd elim (leq_inv_succ1 … H) -H //
+#Z #Y #X #HL12 #H destruct //
+qed-.
+
lemma leq_inv_zero2: ∀I2,K2,L1,V2. L1 ≃[0, 0] K2.ⓑ{I2}V2 →
∃∃I1,K1,V1. K1 ≃[0, 0] K2 & L1 = K1.ⓑ{I1}V1.
#I2 #K2 #L1 #V2 #H elim (leq_inv_zero1 … (leq_sym … H)) -H
(* Basic forward lemmas *****************************************************)
-lemma leq_fwd_length: ∀L1,L2,d,e. L1 ≃[d, e] L2 → |L2| ≤ |L1|.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize /2 width=1 by le_S_S/
+lemma leq_fwd_length: ∀L1,L2,d,e. L1 ≃[d, e] L2 → |L2| = |L1|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize //
qed-.
(* Advanced inversion lemmas ************************************************)
(* *)
(**************************************************************************)
+include "ground_2/ynat/ynat_plus.ma".
include "basic_2/grammar/leq.ma".
(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************)
#I2 #L2 #V2 #HL2 #H destruct /3 width=1 by leq_succ/
]
qed-.
+
+theorem leq_canc_sn: ∀d,e,L,L1,L2. L ≃[d, e] L1 → L ≃[d, e] L2 → L1 ≃[d, e] L2.
+/3 width=3 by leq_trans, leq_sym/ qed-.
+
+theorem leq_canc_dx: ∀d,e,L,L1,L2. L1 ≃[d, e] L → L2 ≃[d, e] L → L1 ≃[d, e] L2.
+/3 width=3 by leq_trans, leq_sym/ qed-.
+
+theorem leq_join: ∀L1,L2,d,i. L1 ≃[d, i] L2 →
+ ∀e. L1 ≃[i+d, e] L2 → L1 ≃[d, i+e] L2.
+#L1 #L2 #d #i #H elim H -L1 -L2 -d -i //
+[ #I #L1 #L2 #V #e #_ #IHL12 #e #H
+ lapply (leq_inv_succ … H ?) -H // >ypred_succ /3 width=1 by leq_pair/
+| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #e #H
+ lapply (leq_inv_succ … H ?) -H // >yplus_succ2 >ypred_succ /3 width=1 by leq_succ/
+]
+qed-.
include "basic_2/notation/relations/pred_4.ma".
include "basic_2/grammar/genv.ma".
-include "basic_2/relocation/lsubr.ma".
+include "basic_2/static/lsubr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
/3 width=6 by leq_trans, step, ex3_intro/
]
qed-.
+
+(* Inversion lemmas on equivalence ******************************************)
+
+lemma ldrop_O_inj: ∀i,L1,L2,K. ⇩[i] L1 ≡ K → ⇩[i] L2 ≡ K → L1 ≃[i, ∞] L2.
+#i @(nat_ind_plus … i) -i
+[ #L1 #L2 #K #H <(ldrop_inv_O2 … H) -K #H <(ldrop_inv_O2 … H) -L1 //
+| #i #IHi * [2: #L1 #I1 #V1 ] * [2,4: #L2 #I2 #V2 ] #K #HLK1 #HLK2 //
+ lapply (ldrop_fwd_length … HLK1)
+ <(ldrop_fwd_length … HLK2) [ /4 width=5 by ldrop_inv_drop1, leq_succ/ ]
+ normalize <plus_n_Sm #H destruct
+]
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/lrsubeq_2.ma".
-include "basic_2/relocation/ldrop.ma".
-
-(* RESTRICTED LOCAL ENVIRONMENT REFINEMENT **********************************)
-
-inductive lsubr: relation lenv ≝
-| lsubr_sort: ∀L. lsubr L (⋆)
-| lsubr_bind: ∀I,L1,L2,V. lsubr L1 L2 → lsubr (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsubr_abst: ∀L1,L2,V,W. lsubr L1 L2 → lsubr (L1.ⓓⓝW.V) (L2.ⓛW)
-.
-
-interpretation
- "local environment refinement (restricted)"
- 'LRSubEq L1 L2 = (lsubr L1 L2).
-
-(* Basic properties *********************************************************)
-
-lemma lsubr_refl: ∀L. L ⊑ L.
-#L elim L -L /2 width=1 by lsubr_sort, lsubr_bind/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lsubr_inv_atom1_aux: ∀L1,L2. L1 ⊑ L2 → L1 = ⋆ → L2 = ⋆.
-#L1 #L2 * -L1 -L2 //
-[ #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V #W #_ #H destruct
-]
-qed-.
-
-lemma lsubr_inv_atom1: ∀L2. ⋆ ⊑ L2 → L2 = ⋆.
-/2 width=3 by lsubr_inv_atom1_aux/ qed-.
-
-fact lsubr_inv_abst1_aux: ∀L1,L2. L1 ⊑ L2 → ∀K1,W. L1 = K1.ⓛW →
- L2 = ⋆ ∨ ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓛW.
-#L1 #L2 * -L1 -L2
-[ #L #K1 #W #H destruct /2 width=1 by or_introl/
-| #I #L1 #L2 #V #HL12 #K1 #W #H destruct /3 width=3 by ex2_intro, or_intror/
-| #L1 #L2 #V1 #V2 #_ #K1 #W #H destruct
-]
-qed-.
-
-lemma lsubr_inv_abst1: ∀K1,L2,W. K1.ⓛW ⊑ L2 →
- L2 = ⋆ ∨ ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓛW.
-/2 width=3 by lsubr_inv_abst1_aux/ qed-.
-
-fact lsubr_inv_abbr2_aux: ∀L1,L2. L1 ⊑ L2 → ∀K2,W. L2 = K2.ⓓW →
- ∃∃K1. K1 ⊑ K2 & L1 = K1.ⓓW.
-#L1 #L2 * -L1 -L2
-[ #L #K2 #W #H destruct
-| #I #L1 #L2 #V #HL12 #K2 #W #H destruct /2 width=3 by ex2_intro/
-| #L1 #L2 #V1 #V2 #_ #K2 #W #H destruct
-]
-qed-.
-
-lemma lsubr_inv_abbr2: ∀L1,K2,W. L1 ⊑ K2.ⓓW →
- ∃∃K1. K1 ⊑ K2 & L1 = K1.ⓓW.
-/2 width=3 by lsubr_inv_abbr2_aux/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lsubr_fwd_length: ∀L1,L2. L1 ⊑ L2 → |L2| ≤ |L1|.
-#L1 #L2 #H elim H -L1 -L2 /2 width=1 by monotonic_le_plus_l/
-qed-.
-
-lemma lsubr_fwd_ldrop2_bind: ∀L1,L2. L1 ⊑ L2 →
- ∀I,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I}W →
- (∃∃K1. K1 ⊑ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I}W) ∨
- ∃∃K1,V. K1 ⊑ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓓⓝW.V & I = Abst.
-#L1 #L2 #H elim H -L1 -L2
-[ #L #I #K2 #W #s #i #H
- elim (ldrop_inv_atom1 … H) -H #H destruct
-| #J #L1 #L2 #V #HL12 #IHL12 #I #K2 #W #s #i #H
- elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
- [ /3 width=3 by ldrop_pair, ex2_intro, or_introl/
- | elim (IHL12 … HLK2) -IHL12 -HLK2 *
- /4 width=4 by ldrop_drop_lt, ex3_2_intro, ex2_intro, or_introl, or_intror/
- ]
-| #L1 #L2 #V1 #V2 #HL12 #IHL12 #I #K2 #W #s #i #H
- elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
- [ /3 width=4 by ldrop_pair, ex3_2_intro, or_intror/
- | elim (IHL12 … HLK2) -IHL12 -HLK2 *
- /4 width=4 by ldrop_drop_lt, ex3_2_intro, ex2_intro, or_introl, or_intror/
- ]
-]
-qed-.
-
-lemma lsubr_fwd_ldrop2_abbr: ∀L1,L2. L1 ⊑ L2 →
- ∀K2,V,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓓV →
- ∃∃K1. K1 ⊑ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓓV.
-#L1 #L2 #HL12 #K2 #V #s #i #HLK2 elim (lsubr_fwd_ldrop2_bind … HL12 … HLK2) -L2 // *
-#K1 #W #_ #_ #H destruct
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/relocation/lsubr.ma".
-
-(* RESTRICTED LOCAL ENVIRONMENT REFINEMENT **********************************)
-
-(* Auxiliary inversion lemmas ***********************************************)
-
-fact lsubr_inv_bind1_aux: ∀L1,L2. L1 ⊑ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
- ∨∨ L2 = ⋆
- | ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓑ{I}X
- | ∃∃K2,V,W. K1 ⊑ K2 & L2 = K2.ⓛW &
- I = Abbr & X = ⓝW.V.
-#L1 #L2 * -L1 -L2
-[ #L #J #K1 #X #H destruct /2 width=1 by or3_intro0/
-| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3 by or3_intro1, ex2_intro/
-| #L1 #L2 #V #W #HL12 #J #K1 #X #H destruct /3 width=6 by or3_intro2, ex4_3_intro/
-]
-qed-.
-
-lemma lsubr_inv_bind1: ∀I,K1,L2,X. K1.ⓑ{I}X ⊑ L2 →
- ∨∨ L2 = ⋆
- | ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓑ{I}X
- | ∃∃K2,V,W. K1 ⊑ K2 & L2 = K2.ⓛW &
- I = Abbr & X = ⓝW.V.
-/2 width=3 by lsubr_inv_bind1_aux/ qed-.
-
-(* Main properties **********************************************************)
-
-theorem lsubr_trans: Transitive … lsubr.
-#L1 #L #H elim H -L1 -L
-[ #L1 #X #H
- lapply (lsubr_inv_atom1 … H) -H //
-| #I #L1 #L #V #_ #IHL1 #X #H
- elim (lsubr_inv_bind1 … H) -H // *
- #L2 [2: #V2 #W2 ] #HL2 #H1 [ #H2 #H3 ] destruct /3 width=1 by lsubr_bind, lsubr_abst/
-| #L1 #L #V1 #W #_ #IHL1 #X #H
- elim (lsubr_inv_abst1 … H) -H // *
- #L2 #HL2 #H destruct /3 width=1 by lsubr_abst/
-]
-qed-.
(**************************************************************************)
include "basic_2/notation/relations/lrsubeqa_3.ma".
-include "basic_2/relocation/lsubr.ma".
+include "basic_2/static/lsubr.ma".
include "basic_2/static/aaa.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
(**************************************************************************)
include "basic_2/notation/relations/lrsubeqd_5.ma".
-include "basic_2/relocation/lsubr.ma".
+include "basic_2/static/lsubr.ma".
include "basic_2/static/da.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR DEGREE ASSIGNMENT ***********************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/lrsubeq_2.ma".
+include "basic_2/relocation/ldrop.ma".
+
+(* RESTRICTED LOCAL ENVIRONMENT REFINEMENT **********************************)
+
+inductive lsubr: relation lenv ≝
+| lsubr_sort: ∀L. lsubr L (⋆)
+| lsubr_bind: ∀I,L1,L2,V. lsubr L1 L2 → lsubr (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lsubr_abst: ∀L1,L2,V,W. lsubr L1 L2 → lsubr (L1.ⓓⓝW.V) (L2.ⓛW)
+.
+
+interpretation
+ "local environment refinement (restricted)"
+ 'LRSubEq L1 L2 = (lsubr L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lsubr_refl: ∀L. L ⊑ L.
+#L elim L -L /2 width=1 by lsubr_sort, lsubr_bind/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubr_inv_atom1_aux: ∀L1,L2. L1 ⊑ L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 * -L1 -L2 //
+[ #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #_ #H destruct
+]
+qed-.
+
+lemma lsubr_inv_atom1: ∀L2. ⋆ ⊑ L2 → L2 = ⋆.
+/2 width=3 by lsubr_inv_atom1_aux/ qed-.
+
+fact lsubr_inv_abst1_aux: ∀L1,L2. L1 ⊑ L2 → ∀K1,W. L1 = K1.ⓛW →
+ L2 = ⋆ ∨ ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓛW.
+#L1 #L2 * -L1 -L2
+[ #L #K1 #W #H destruct /2 width=1 by or_introl/
+| #I #L1 #L2 #V #HL12 #K1 #W #H destruct /3 width=3 by ex2_intro, or_intror/
+| #L1 #L2 #V1 #V2 #_ #K1 #W #H destruct
+]
+qed-.
+
+lemma lsubr_inv_abst1: ∀K1,L2,W. K1.ⓛW ⊑ L2 →
+ L2 = ⋆ ∨ ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓛW.
+/2 width=3 by lsubr_inv_abst1_aux/ qed-.
+
+fact lsubr_inv_abbr2_aux: ∀L1,L2. L1 ⊑ L2 → ∀K2,W. L2 = K2.ⓓW →
+ ∃∃K1. K1 ⊑ K2 & L1 = K1.ⓓW.
+#L1 #L2 * -L1 -L2
+[ #L #K2 #W #H destruct
+| #I #L1 #L2 #V #HL12 #K2 #W #H destruct /2 width=3 by ex2_intro/
+| #L1 #L2 #V1 #V2 #_ #K2 #W #H destruct
+]
+qed-.
+
+lemma lsubr_inv_abbr2: ∀L1,K2,W. L1 ⊑ K2.ⓓW →
+ ∃∃K1. K1 ⊑ K2 & L1 = K1.ⓓW.
+/2 width=3 by lsubr_inv_abbr2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lsubr_fwd_length: ∀L1,L2. L1 ⊑ L2 → |L2| ≤ |L1|.
+#L1 #L2 #H elim H -L1 -L2 /2 width=1 by monotonic_le_plus_l/
+qed-.
+
+lemma lsubr_fwd_ldrop2_bind: ∀L1,L2. L1 ⊑ L2 →
+ ∀I,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I}W →
+ (∃∃K1. K1 ⊑ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I}W) ∨
+ ∃∃K1,V. K1 ⊑ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓓⓝW.V & I = Abst.
+#L1 #L2 #H elim H -L1 -L2
+[ #L #I #K2 #W #s #i #H
+ elim (ldrop_inv_atom1 … H) -H #H destruct
+| #J #L1 #L2 #V #HL12 #IHL12 #I #K2 #W #s #i #H
+ elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
+ [ /3 width=3 by ldrop_pair, ex2_intro, or_introl/
+ | elim (IHL12 … HLK2) -IHL12 -HLK2 *
+ /4 width=4 by ldrop_drop_lt, ex3_2_intro, ex2_intro, or_introl, or_intror/
+ ]
+| #L1 #L2 #V1 #V2 #HL12 #IHL12 #I #K2 #W #s #i #H
+ elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
+ [ /3 width=4 by ldrop_pair, ex3_2_intro, or_intror/
+ | elim (IHL12 … HLK2) -IHL12 -HLK2 *
+ /4 width=4 by ldrop_drop_lt, ex3_2_intro, ex2_intro, or_introl, or_intror/
+ ]
+]
+qed-.
+
+lemma lsubr_fwd_ldrop2_abbr: ∀L1,L2. L1 ⊑ L2 →
+ ∀K2,V,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓓV →
+ ∃∃K1. K1 ⊑ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓓV.
+#L1 #L2 #HL12 #K2 #V #s #i #HLK2 elim (lsubr_fwd_ldrop2_bind … HL12 … HLK2) -L2 // *
+#K1 #W #_ #_ #H destruct
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/static/lsubr.ma".
+
+(* RESTRICTED LOCAL ENVIRONMENT REFINEMENT **********************************)
+
+(* Auxiliary inversion lemmas ***********************************************)
+
+fact lsubr_inv_bind1_aux: ∀L1,L2. L1 ⊑ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
+ ∨∨ L2 = ⋆
+ | ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓑ{I}X
+ | ∃∃K2,V,W. K1 ⊑ K2 & L2 = K2.ⓛW &
+ I = Abbr & X = ⓝW.V.
+#L1 #L2 * -L1 -L2
+[ #L #J #K1 #X #H destruct /2 width=1 by or3_intro0/
+| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3 by or3_intro1, ex2_intro/
+| #L1 #L2 #V #W #HL12 #J #K1 #X #H destruct /3 width=6 by or3_intro2, ex4_3_intro/
+]
+qed-.
+
+lemma lsubr_inv_bind1: ∀I,K1,L2,X. K1.ⓑ{I}X ⊑ L2 →
+ ∨∨ L2 = ⋆
+ | ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓑ{I}X
+ | ∃∃K2,V,W. K1 ⊑ K2 & L2 = K2.ⓛW &
+ I = Abbr & X = ⓝW.V.
+/2 width=3 by lsubr_inv_bind1_aux/ qed-.
+
+(* Main properties **********************************************************)
+
+theorem lsubr_trans: Transitive … lsubr.
+#L1 #L #H elim H -L1 -L
+[ #L1 #X #H
+ lapply (lsubr_inv_atom1 … H) -H //
+| #I #L1 #L #V #_ #IHL1 #X #H
+ elim (lsubr_inv_bind1 … H) -H // *
+ #L2 [2: #V2 #W2 ] #HL2 #H1 [ #H2 #H3 ] destruct /3 width=1 by lsubr_bind, lsubr_abst/
+| #L1 #L #V1 #W #_ #IHL1 #X #H
+ elim (lsubr_inv_abst1 … H) -H // *
+ #L2 #HL2 #H destruct /3 width=1 by lsubr_abst/
+]
+qed-.
include "basic_2/notation/relations/lazyeqalt_4.ma".
include "basic_2/substitution/lleq_lleq.ma".
+(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
+
+(* Note: alternative definition of lleq *)
inductive lleqa: relation4 ynat term lenv lenv ≝
| lleqa_sort: ∀L1,L2,d,k. |L1| = |L2| → lleqa d (⋆k) L1 L2
| lleqa_skip: ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → lleqa d (#i) L1 L2
/3 width=4 by lleq_sym, ex2_2_intro/
qed-.
-lemma lleq_inv_lref_ge: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
- ∀I1,I2,K1,K2,V.
- ⇩[i] L1 ≡ K1.ⓑ{I1}V → ⇩[i] L2 ≡ K2.ⓑ{I2}V → K1 ⋕[V, 0] K2.
-#L1 #L2 #d #i #HL12 #Hdi #I1 #I2 #K1 #K2 #V #HLK1 #HLK2
+lemma lleq_inv_lref_ge_gen: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
+ ∀I1,I2,K1,K2,V1,V2.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ V1 = V2 ∧ K1 ⋕[V2, 0] K2.
+#L1 #L2 #d #i #HL12 #Hdi #I1 #I2 #K1 #K2 #V1 #V2 #HLK1 #HLK2
elim (lleq_inv_lref_ge_sn … HL12 … HLK1) // -L1 -d
-#J #Y #HY lapply (ldrop_mono … HY … HLK2) -L2 -i #H destruct //
+#J #Y #HY lapply (ldrop_mono … HY … HLK2) -L2 -i #H destruct /2 width=1 by conj/
+qed-.
+
+lemma lleq_inv_lref_ge: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
+ ∀I,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V →
+ K1 ⋕[V, 0] K2.
+#L1 #L2 #d #i #HL12 #Hdi #I #K1 #K2 #V #HLK1 #HLK2
+elim (lleq_inv_lref_ge_gen … HL12 … HLK1 HLK2) //
qed-.
(* Advanced properties ******************************************************)
[ "sh" "sd" * ]
}
]
+ [ { "restricted local env. ref." * } {
+ [ "lsubr ( ? ⊑ ? )" "lsubr_lsubr" * ]
+ }
+ ]
}
]
class "yellow"
[ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_cpy" * ]
}
]
- [ { "restricted local env. ref." * } {
- [ "lsubr ( ? ⊑ ? )" "lsubr_lsubr" * ]
- }
- ]
[ { "local env. ref. for extended substitution" * } {
[ "lsuby ( ? ⊑×[?,?] ? )" "lsuby_lsuby" * ]
}
projects / helm.git / commitdiff