- ∀Q:predicate term.
- (∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 →
- (∀T2. ❪G,L❫ ⊢ T1 ⬈* T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1
- ) →
- ∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 →
- ∀T2. ❪G,L❫ ⊢ T1 ⬈* T2 → Q T2.
+ ∀Q:predicate term.
+ (∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 →
+ (∀T2. ❪G,L❫ ⊢ T1 ⬈* T2 → (T1 ≅ T2 → ⊥) → Q T2) → Q T1
+ ) →
+ ∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 →
+ ∀T2. ❪G,L❫ ⊢ T1 ⬈* T2 → Q T2.