(* Basic_1: was: nf2_pr3_unfold *)
(* Basic_2A1: was: cprs_inv_cnr1 *)
lemma cprs_inv_cnr_sn (h) (G) (L):
- â\88\80T1,T2. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡*[h] T2 â\86\92 â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] ð\9d\90\8dâ\9dªT1â\9d« → T1 = T2.
+ â\88\80T1,T2. â\9d¨G,Lâ\9d© â\8a¢ T1 â\9e¡*[h,0] T2 â\86\92 â\9d¨G,Lâ\9d© â\8a¢ â\9e¡ð\9d\90\8d[h,0] T1 → T1 = T2.
#h #G #L #T1 #T2 #H @(cprs_ind_sn … H) -T1 //
#T1 #T0 #HT10 #_ #IH #HT1
lapply (HT1 … HT10) -HT10 #H destruct /2 width=1 by/