(* Basic_2A1: uses: lsx_ind *)
lemma rsx_ind (G) (T) (Q:predicate …):
(∀L1. G ⊢ ⬈*𝐒[T] L1 →
- (â\88\80L2. â\9dªG,L1â\9d« ⊢ ⬈ L2 → (L1 ≅[T] L2 → ⊥) → Q L2) →
+ (â\88\80L2. â\9d¨G,L1â\9d© ⊢ ⬈ L2 → (L1 ≅[T] L2 → ⊥) → Q L2) →
Q L1
) →
∀L. G ⊢ ⬈*𝐒[T] L → Q L.
(* Basic_2A1: uses: lsx_intro *)
lemma rsx_intro (G) (T):
∀L1.
- (â\88\80L2. â\9dªG,L1â\9d« ⊢ ⬈ L2 → (L1 ≅[T] L2 → ⊥) → G ⊢ ⬈*𝐒[T] L2) →
+ (â\88\80L2. â\9d¨G,L1â\9d© ⊢ ⬈ L2 → (L1 ≅[T] L2 → ⊥) → G ⊢ ⬈*𝐒[T] L2) →
G ⊢ ⬈*𝐒[T] L1.
/5 width=1 by SN_intro/ qed.