(* *)
(**************************************************************************)
-include "basic_2/reducibility/cpr.ma".
include "basic_2/reducibility/cnf.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
/4 width=1/ qed.
(* Basic_1: was: sn3_nf2 *)
-lemma csn_cnf: ∀L,T. L ⊢ 𝐍[T] → L ⊢ ⬇* T.
+lemma csn_cnf: ∀L,T. L ⊢ 𝐍⦃T⦄ → L ⊢ ⬇* T.
/2 width=1/ qed.
lemma csn_cpr_trans: ∀L,T1. L ⊢ ⬇* T1 → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ ⬇* T2.
qed.
(* Basic_1: was: sn3_cast *)
-lemma csn_cast: â\88\80L,W. L â\8a¢ â¬\87* W â\86\92 â\88\80T. L â\8a¢ â¬\87* T â\86\92 L â\8a¢ â¬\87* â\93£W. T.
+lemma csn_cast: â\88\80L,W. L â\8a¢ â¬\87* W â\86\92 â\88\80T. L â\8a¢ â¬\87* T â\86\92 L â\8a¢ â¬\87* â\93\9dW. T.
#L #W #HW elim HW -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT
@csn_intro #X #H1 #H2
elim (cpr_inv_cast1 … H1) -H1