- | tshf_abst: ∀V1,V2,T1,T2. tshf (ⓛV1. T1) (ⓛV2. T2)
- | tshf_appl: ∀V1,V2,T1,T2. tshf T1 T2 → 𝐒[T1] → 𝐒[T2] →
+ | tshf_abbr: ∀V1,V2,T1,T2. tshf (-ⓓV1. T1) (-ⓓV2. T2)
+ | tshf_abst: ∀a,V1,V2,T1,T2. tshf (ⓛ{a}V1. T1) (ⓛ{a}V2. T2)
+ | tshf_appl: ∀V1,V2,T1,T2. tshf T1 T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄ →