Nuprl Lemma : bool_wf
𝔹 ∈ Type
Proof
Definitions occuring in Statement :
bool: 𝔹,
member: t ∈ T,
universe: Type
Definitions unfolded in proof :
bool: 𝔹,
member: t ∈ T
Lemmas referenced :
unit_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
unionEquality,
because_Cache,
cut,
lemma_by_obid,
hypothesis
Latex:
\mBbbB{} \mmember{} Type
Date html generated:
2016_05_13-PM-03_20_02
Last ObjectModification:
2015_12_26-AM-09_09_44
Theory : basic_types
Home
Index