Nuprl Rule : classicalIntroduction
This rule proved as lemma rule_classical_introduction_true3 in file rules/rules_classical.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ {x:Unit| P}
BY classicalIntroduction !parameter{i:l} z ()
H ⊢ P = P ∈ Type
H z:(P ⟶ Void) @i ⊢ Void
Definitions occuring in rule :
set: {x:A| B[x]} ,
unit: Unit,
equal: s = t ∈ T,
universe: Type,
function: x:A ⟶ B[x],
void: Void,
axiom: Ax
Latex:
H \mvdash{} \{x:Unit| P\}
BY classicalIntroduction !parameter\{i:l\} z ()
H \mvdash{} P = P
H z:(P {}\mrightarrow{} Void) @i \mvdash{} Void
Date html generated:
2017_09_29-PM-05_45_01
Last ObjectModification:
2016_07_08-PM-03_49_02
Theory : rules
Home
Index