(* *)
(**************************************************************************)
-include "Basic_2/grammar/tstc_tstc.ma".
-include "Basic_2/computation/cprs_cprs.ma".
-include "Basic_2/computation/csn_lift.ma".
-include "Basic_2/computation/csn_cpr.ma".
-include "Basic_2/computation/csn_cprs.ma".
+include "basic_2/grammar/tstc_tstc.ma".
+include "basic_2/computation/cprs_cprs.ma".
+include "basic_2/computation/csn_lift.ma".
+include "basic_2/computation/csn_cpr.ma".
+include "basic_2/computation/csn_cprs.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
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.