Nuprl Lemma : unit_triviality

[a:Unit]. (a = ⋅ ∈ Unit)


Proof




Definitions occuring in Statement :  it: uall: [x:A]. B[x] unit: Unit equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] unit: Unit member: t ∈ T it:
Lemmas referenced :  it_wf unit_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  sqequalHypSubstitution equalityElimination thin cut introduction extract_by_obid hypothesis Error :universeIsType

Latex:
\mforall{}[a:Unit].  (a  =  \mcdot{})



Date html generated: 2019_06_20-AM-11_14_50
Last ObjectModification: 2018_09_26-AM-10_42_02

Theory : core_2


Home Index