qed.
(* Basic_1: was: sn3_beta *)
-lemma csn_appl_beta: ∀L,W. L ⊢ ⬇* W → ∀V,T. L ⊢ ⬇* (ⓓV. T) → (**)
+lemma csn_appl_beta: ∀L,W. L ⊢ ⬇* W → ∀V,T. L ⊢ ⬇* ⓓV. T →
L ⊢ ⬇* ⓐV. ⓛW. T.
/2 width=3/ qed.
]
qed.
-(* Basic_1: was: sn3_appl_bind *)
lemma csn_appl_theta: ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
∀L,V,T. L ⊢ ⬇* ⓓV. ⓐV2. T → L ⊢ ⬇* ⓐV1. ⓓV. T.
/2 width=5/ qed.