Nuprl Lemma : istype-base

istype(Base)


Proof




Definitions occuring in Statement :  base: Base
Definitions unfolded in proof :  member: t ∈ T
Lemmas referenced :  base_wf
Rules used in proof :  Error :universeIsType,  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut introduction extract_by_obid hypothesis

Latex:
istype(Base)



Date html generated: 2019_06_20-AM-11_13_34
Last ObjectModification: 2018_09_28-PM-01_05_56

Theory : core_2


Home Index