(* Note: this is Tait's iii, or Girard's CR4 *)
definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→predicate term.
∀L,Vs. all … (RP L) Vs →
- ∀T. 𝐒[T] → NF … (RR L) RS T → C L (ⒶVs.T).
+ ∀T. 𝐒⦃T⦄ → NF … (RR L) RS T → C L (ⒶVs.T).
(* Note: this is Tait's ii *)
definition S3 ≝ λRP,C:lenv→predicate term.
∀V,T. C (L. ⓓV) (ⒶV2s. T) → RP L V → C L (ⒶV1s. ⓓV. T).
definition S6 ≝ λRP,C:lenv→predicate term.
- â\88\80L,Vs,T,W. C L (â\92¶Vs. T) â\86\92 RP L W â\86\92 C L (â\92¶Vs. â\93£W. T).
+ â\88\80L,Vs,T,W. C L (â\92¶Vs. T) â\86\92 RP L W â\86\92 C L (â\92¶Vs. â\93\9dW. T).
definition S7 ≝ λC:lenv→predicate term. ∀L2,L1,T1,d,e.
C L1 T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2.