(* Basic_1: was: nf2_dec *)
(* Basic_2A1: uses: cnr_dec *)
lemma cnr_dec_teqx (h) (G) (L):
- ∀T1. ∨∨ ❪G,L❫ ⊢ ➡[h] 𝐍❪T1❫
- | ∃∃T2. ❪G,L❫ ⊢ T1 ➡[h] T2 & (T1 ≛ T2 → ⊥).
+ ∀T1. ∨∨ ❪G,L❫ ⊢ ➡𝐍[h,0] T1
+ | ∃∃T2. ❪G,L❫ ⊢ T1 ➡[h,0] T2 & (T1 ≛ T2 → ⊥).
#h #G #L #T1
@(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1 #G0 #L0 #T0 #IH #G #L * *
[ #s #HG #HL #HT destruct -IH