(* *)
(**************************************************************************)
-include "Basic_2/static/lsuba.ma".
+include "basic_2/static/lsuba.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
(* Properties concerning basic local environment slicing ********************)
(* Note: the constant 0 cannot be generalized *)
-
-lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ÷⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 →
- ∃∃K2. K1 ÷⊑ K2 & ⇩[0, e] L2 ≡ K2.
+lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ⁝⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 →
+ ∃∃K2. K1 ⁝⊑ K2 & ⇩[0, e] L2 ≡ K2.
#L1 #L2 #H elim H -L1 -L2
[ /2 width=3/
| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
]
qed-.
-lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ÷⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
- ∃∃K1. K1 ÷⊑ K2 & ⇩[0, e] L1 ≡ K1.
+(* Note: the constant 0 cannot be generalized *)
+lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ⁝⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+ ∃∃K1. K1 ⁝⊑ K2 & ⇩[0, e] L1 ≡ K1.
#L1 #L2 #H elim H -L1 -L2
[ /2 width=3/
| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H