(* Properties with normal forms *********************************************)
lemma cpxs_cnx (h) (G) (L) (T1):
- (â\88\80T2. â¦\83G,Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 T1 â\89\9b T2) â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â¬\88[h] ð\9d\90\8dâ¦\83T1â¦\84.
+ (â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88*[h] T2 â\86\92 T1 â\89\9b T2) â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88ð\9d\90\8d[h] T1.
/3 width=1 by cpx_cpxs/ qed.
(* Inversion lemmas with normal terms ***************************************)
lemma cpxs_inv_cnx1 (h) (G) (L):
- â\88\80T1,T2. â¦\83G,Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â¬\88[h] ð\9d\90\8dâ¦\83T1â¦\84 → T1 ≛ T2.
+ â\88\80T1,T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88*[h] T2 â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88ð\9d\90\8d[h] T1 → T1 ≛ T2.
#h #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
-/5 width=9 by cnx_tdeq_trans, tdeq_trans/
+/5 width=9 by cnx_teqx_trans, teqx_trans/
qed-.