Nuprl Lemma : unit_wf2
Unit ∈ Type
Proof
Definitions occuring in Statement :
unit: Unit,
member: t ∈ T,
universe: Type
Definitions unfolded in proof :
member: t ∈ T
Lemmas referenced :
unit_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
lemma_by_obid,
hypothesis
Latex:
Unit \mmember{} Type
Date html generated:
2016_05_13-PM-03_21_44
Last ObjectModification:
2015_12_26-AM-09_32_01
Theory : call!by!value_1
Home
Index