(* Properties with normal forms *********************************************)
lemma cpxs_cnx (h) (G) (L) (T1):
(* Properties with normal forms *********************************************)
lemma cpxs_cnx (h) (G) (L) (T1):
/3 width=1 by cpx_cpxs/ qed.
(* Inversion lemmas with normal terms ***************************************)
lemma cpxs_inv_cnx1 (h) (G) (L):
/3 width=1 by cpx_cpxs/ qed.
(* Inversion lemmas with normal terms ***************************************)
lemma cpxs_inv_cnx1 (h) (G) (L):
- ∀T1,T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → ❪G,L❫ ⊢ ⬈[h] 𝐍❪T1❫ → T1 ≛ T2.
+ ∀T1,T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → ❪G,L❫ ⊢ ⬈𝐍[h] T1 → T1 ≛ T2.
#h #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
/5 width=9 by cnx_teqx_trans, teqx_trans/
qed-.
#h #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
/5 width=9 by cnx_teqx_trans, teqx_trans/
qed-.