- ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[T] L2 → ⊥) →
- ∃∃L,L0. ⦃G, L1⦄ ⊢ ⬈[h] L & L1 ≛[T] L → ⊥ &
- ⦃G, L⦄ ⊢ ⬈*[h] L0 & L0 ≛[T] L2.
+ ∀L1,L2. ⦃G,L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[T] L2 → ⊥) →
+ ∃∃L,L0. ⦃G,L1⦄ ⊢ ⬈[h] L & L1 ≛[T] L → ⊥ &
+ ⦃G,L⦄ ⊢ ⬈*[h] L0 & L0 ≛[T] L2.