(* Properties with atomic arity assignment for terms ************************)
lemma cpts_total_aaa (h) (G) (L) (T1):
- â\88\80A. â¦\83G,Lâ¦\84 â\8a¢ T1 â\81\9d A â\86\92 â\88\80n. â\88\83T2. â¦\83G,Lâ¦\84 ⊢ T1 ⬆*[h,n] T2.
+ â\88\80A. â\9dªG,Lâ\9d« â\8a¢ T1 â\81\9d A â\86\92 â\88\80n. â\88\83T2. â\9dªG,Lâ\9d« ⊢ T1 ⬆*[h,n] T2.
#h #G #L #T1 #A #H elim H -G -L -T1 -A
[ #G #L #s #n /3 width=2 by ex_intro/
| #I #G #K #V1 #B #_ #IH #n -B
cases I -I
[ elim (IH n) -IH #V2 #HV12
- elim (lifts_total V2 (ð\9d\90\94â\9d´1â\9dµ)) #T2 #HVT2
+ elim (lifts_total V2 (ð\9d\90\94â\9d¨1â\9d©)) #T2 #HVT2
/3 width=4 by cpts_delta, ex_intro/
| cases n -n
[ /2 width=2 by ex_intro/
| #n elim (IH n) -IH #V2 #HV12
- elim (lifts_total V2 (ð\9d\90\94â\9d´1â\9dµ)) #T2 #HVT2
+ elim (lifts_total V2 (ð\9d\90\94â\9d¨1â\9d©)) #T2 #HVT2
/3 width=4 by cpts_ell, ex_intro/
]
]
| #I #G #K #A #i #_ #IH #n -A
elim (IH n) -IH #T #HT
- elim (lifts_total T (ð\9d\90\94â\9d´1â\9dµ)) #U #HTU
+ elim (lifts_total T (ð\9d\90\94â\9d¨1â\9d©)) #U #HTU
/3 width=4 by cpts_lref, ex_intro/
| #p #G #L #V1 #T1 #B #A #_ #_ #IHV #IHT #n -B -A
elim (IHV 0) -IHV #V2 #HV12