(* Properties with normal forms *********************************************)
lemma cpxs_cnx (G) (L) (T1):
(* Properties with normal forms *********************************************)
lemma cpxs_cnx (G) (L) (T1):
- (â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88* T2 â\86\92 T1 â\89\85 T2) â\86\92 â\9dªG,Lâ\9d« ⊢ ⬈𝐍 T1.
+ (â\88\80T2. â\9d¨G,Lâ\9d© â\8a¢ T1 â¬\88* T2 â\86\92 T1 â\89\85 T2) â\86\92 â\9d¨G,Lâ\9d© ⊢ ⬈𝐍 T1.
/3 width=1 by cpx_cpxs/ qed.
(* Inversion lemmas with normal terms ***************************************)
lemma cpxs_inv_cnx1 (G) (L):
/3 width=1 by cpx_cpxs/ qed.
(* Inversion lemmas with normal terms ***************************************)
lemma cpxs_inv_cnx1 (G) (L):
- â\88\80T1,T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88* T2 â\86\92 â\9dªG,Lâ\9d« ⊢ ⬈𝐍 T1 → T1 ≅ T2.
+ â\88\80T1,T2. â\9d¨G,Lâ\9d© â\8a¢ T1 â¬\88* T2 â\86\92 â\9d¨G,Lâ\9d© ⊢ ⬈𝐍 T1 → T1 ≅ T2.
#G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
/5 width=9 by cnx_teqx_trans, teqx_trans/
qed-.
#G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
/5 width=9 by cnx_teqx_trans, teqx_trans/
qed-.