(* Basic_1: was: nf2_dec *)
(* Basic_2A1: uses: cnr_dec *)
lemma cnr_dec_tdeq (h) (G) (L):
- ∀T1. ∨∨ ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃T1⦄
- | ∃∃T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 & (T1 ≛ T2 → ⊥).
+ ∀T1. ∨∨ ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃T1⦄
+ | ∃∃T2. ⦃G,L⦄ ⊢ T1 ➡[h] 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
elim (tdeq_inv_pair … H) -H #H destruct
| @or_intror @(ex2_intro … (ⓓ{p}ⓝW1.V1.U1)) [ /2 width=1 by cpm_beta/ ] #H
elim (tdeq_inv_pair … H) -H #H destruct
- ]
+ ]
| #T2 #HT12 #HnT12 #_
@or_intror @(ex2_intro … (ⓐV1.T2)) [ /2 width=1 by cpm_appl/ ] #H
elim (tdeq_inv_pair … H) -H /2 width=1 by/