(* Forward lemmas on atomic arity assignment for terms **********************)
-lemma snv_fwd_aaa: â\88\80h,g,L,T. â¦\83h, Lâ¦\84 â\8a© T :[g] → ∃A. L ⊢ T ⁝ A.
+lemma snv_fwd_aaa: â\88\80h,g,L,T. â¦\83h, Lâ¦\84 â\8a¢ T ¡[g] → ∃A. L ⊢ T ⁝ A.
#h #g #L #T #H elim H -L -T
[ /2 width=2/
| #I #L #K #V #i #HLK #_ * /3 width=6/
]
qed-.
-lemma snv_fwd_csn: â\88\80h,g,L,T. â¦\83h, Lâ¦\84 â\8a© T :[g] → L ⊢ ⬊* T.
+lemma snv_fwd_csn: â\88\80h,g,L,T. â¦\83h, Lâ¦\84 â\8a¢ T ¡[g] → L ⊢ ⬊* T.
#h #g #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/
qed-.