(**************************************************************************)
include "basic_2/notation/relations/predtystrong_5.ma".
(**************************************************************************)
include "basic_2/notation/relations/predtystrong_5.ma".
include "basic_2/rt_transition/cpx.ma".
(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
include "basic_2/rt_transition/cpx.ma".
(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
-lemma csx_ind: ∀h,o,G,L. ∀R:predicate term.
+lemma csx_ind: ∀h,o,G,L. ∀Q:predicate term.
- ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T.
-#h #o #G #L #R #H0 #T1 #H elim H -T1
+ ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → Q T.
+#h #o #G #L #Q #H0 #T1 #H elim H -T1