H
O
L
-
N
ominal-
E
xamples
Class1
Class2
Class3
CK_Machine
Compile
Contexts
Crary
CR_Takahashi
Lam_Funs
CR
Fsub
Height
Lambda_mu
LocalWeakening
Pattern
SN
SOS
Standardization
Support
Type_Preservation
Weakening
W
VC_Condition