(* Forward lemmas with t-bound rt-transition for terms **********************)
lemma cpt_fwd_cpm (h) (n) (G) (L):
- â\88\80T1,T2. â¦\83G,Lâ¦\84 â\8a¢ T1 â¬\86[h,n] T2 â\86\92 â¦\83G,Lâ¦\84 ⊢ T1 ➡[n,h] T2.
+ â\88\80T1,T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\86[h,n] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ T1 ➡[n,h] T2.
#h #n #G #L #T1 #T2 #H
@(cpt_ind … H) -n -G -L -T1 -T2
/3 width=3 by cpm_ee, cpm_cast, cpm_appl, cpm_bind, cpm_lref, cpm_ell, cpm_delta/