interpretation
"local environment refinement (substitution)"
- 'SubEq L1 L2 = (lsubr L1 L2).
-
-definition lsubr_trans: ∀S. predicate (lenv → relation S) ≝ λS,R.
- ∀L2,s1,s2. R L2 s1 s2 → ∀L1. L1 ⊑ L2 → R L1 s1 s2.
+ 'CrSubEq L1 L2 = (lsubr L1 L2).
(* Basic properties *********************************************************)
#L elim L -L // /2 width=1/
qed.
-lemma TC_lsubr_trans: ∀S,R. lsubr_trans S R → lsubr_trans S (LTC … R).
-#S #R #HR #L1 #s1 #s2 #H elim H -s2
-[ /3 width=3/
-| #s #s2 #_ #Hs2 #IHs1 #L2 #HL12
- lapply (HR … Hs2 … HL12) -HR -Hs2 /3 width=3/
-]
-qed.
-
(* Basic inversion lemmas ***************************************************)
fact lsubr_inv_atom1_aux: ∀L1,L2. L1 ⊑ L2 → L1 = ⋆ → L2 = ⋆.
∃∃K1. K1 ⊑ K2 & ⇩[0, i] L1 ≡ K1. ⓓW.
#L1 #L2 #H elim H -L1 -L2
[ #L #K2 #W #i #H
- lapply (ldrop_inv_atom1 … H) -H #H destruct
+ elim (ldrop_inv_atom1 … H) -H #H destruct
| #L1 #L2 #V #HL12 #IHL12 #K2 #W #i #H
- elim (ldrop_inv_O1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
+ elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
[ /2 width=3/
| elim (IHL12 … HLK2) -IHL12 -HLK2 /3 width=3/
]
| #I #L1 #L2 #V1 #V2 #_ #IHL12 #K2 #W #i #H
- elim (ldrop_inv_O1 … H) -H * #Hi #HLK2 destruct
+ elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct
elim (IHL12 … HLK2) -IHL12 -HLK2 /3 width=3/
]
qed-.