(* 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.
lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
∀L,W,T,A,B. RP L W → (
∀L0,V0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des + 1] T ≡ T0 →
- ⦃L0, V0⦄ [RP] ϵ 〚B〛 → ⦃L0. ⓓV0, T0⦄ [RP] ϵ 〚A〛
+ ⦃L0, V0⦄ ϵ[RP] 〚B〛 → ⦃L0. ⓓV0, T0⦄ ϵ[RP] 〚A〛
) →
- ⦃L, ⓛW. T⦄ [RP] ϵ 〚②B. A〛.
+ ⦃L, ⓛW. T⦄ ϵ[RP] 〚②B. A〛.
#RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H
lapply (aacr_acr … H1RP H2RP A) #HCA
lapply (aacr_acr … H1RP H2RP B) #HCB