(* Properties with atomic arity assignment for terms ************************)
lemma cpts_total_aaa (h) (G) (L) (T1):
- â\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.
+ â\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