Nuprl Lemma : vr_test_foo_bar345566546
1 + 𝔹 ∈ Void ⟶ 1
Proof
Definitions occuring in Statement :
bool: 𝔹,
member: t ∈ T,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n,
void: Void
Definitions unfolded in proof :
member: t ∈ T
Lemmas referenced :
void_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
functionExtensionality,
voidElimination,
cut,
instantiate,
lemma_by_obid,
hypothesis
Latex:
1 + \mBbbB{} \mmember{} Void {}\mrightarrow{} 1
Date html generated:
2016_05_15-PM-07_56_56
Last ObjectModification:
2015_12_27-AM-11_04_12
Theory : general
Home
Index