Nuprl Lemma : decidable__false
Dec(False)
Proof
Definitions occuring in Statement :
decidable: Dec(P),
false: False
Definitions unfolded in proof :
decidable: Dec(P),
or: P ∨ Q,
not: ¬A,
implies: P ⇒ Q,
false: False,
member: t ∈ T,
prop: ℙ
Lemmas referenced :
false_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
inrFormation,
lambdaFormation,
sqequalHypSubstitution,
voidElimination,
cut,
lemma_by_obid,
hypothesis
Latex:
Dec(False)
Date html generated:
2016_05_13-PM-03_09_08
Last ObjectModification:
2016_01_06-PM-05_27_12
Theory : core_2
Home
Index