-lemma rdsx_ind_lpxs_lfdeq (h) (o) (G):
- ∀T. ∀Q:predicate lenv.
- (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → Q L2) →
- Q L1
- ) →
- ∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h] L0 → ∀L2. L0 ≛[h, o, T] L2 → Q L2.
+lemma rdsx_ind_lpxs_rdeq (h) (o) (G):
+ ∀T. ∀Q:predicate lenv.
+ (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → Q L2) →
+ Q L1
+ ) →
+ ∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h] L0 → ∀L2. L0 ≛[h, o, T] L2 → Q L2.