Nuprl Rule : levelHypothesis
H x:A @i, J ⊢ A = A ∈ Type
BY levelHypothesis #$h
No Subgoals
Latex:
H x:A @i, J \mvdash{} A = A
BY levelHypothesis \#\$h
No Subgoals
Date html generated:
2019_06_20-PM-04_11_50
Last ObjectModification:
2015_11_25-PM-03_37_48
Theory : rules
Home
Index