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