rho:(Label
Type). st_lift(rho) 
(Label+Unit)Type Type| Who Cites st lift? | |
| st_lift | Def st_lift(rho)(x) == InjCase(x; x'. rho(x'); a. Top) |
| Thm* rho:(LabelType). st_lift(rho) (Label+Unit)Type | |
| top | Def Top == Void given Void |
| Thm* Top Type |
About:
 |  |  |  |  |
 |  |  |  |  |  |  |