-| tweq_abbr: ∀p,V1,V2,T1,T2. (p=Ⓣ→tweq T1 T2) → tweq (ⓓ{p}V1.T1) (ⓓ{p}V2.T2)
-| tweq_abst: ∀p,V1,V2,T1,T2. tweq (ⓛ{p}V1.T1) (ⓛ{p}V2.T2)
+| tweq_abbr: ∀p,V1,V2,T1,T2. (p=Ⓣ→tweq T1 T2) → tweq (ⓓ[p]V1.T1) (ⓓ[p]V2.T2)
+| tweq_abst: ∀p,V1,V2,T1,T2. tweq (ⓛ[p]V1.T1) (ⓛ[p]V2.T2)