- | thom_atom: ∀I. thom (𝕒{I}) (𝕒{I})
- | thom_abst: ∀V1,V2,T1,T2. thom (𝕔{Abst} V1. T1) (𝕔{Abst} V2. T2)
- | thom_appl: â\88\80V1,V2,T1,T2. thom T1 T2 â\86\92 ð\9d\95\8a[T1] â\86\92 ð\9d\95\8a[T2] →
- thom (𝕔{Appl} V1. T1) (𝕔{Appl} V2. T2)
+ | thom_atom: ∀I. thom (⓪{I}) (⓪{I})
+ | thom_abst: ∀V1,V2,T1,T2. thom (ⓛV1. T1) (ⓛV2. T2)
+ | thom_appl: â\88\80V1,V2,T1,T2. thom T1 T2 â\86\92 ð\9d\90\92[T1] â\86\92 ð\9d\90\92[T2] →
+ thom (ⓐV1. T1) (ⓐV2. T2)