Nuprl Lemma : gen_hyp_tp

[A:Type]. ∀[e:A]. ∀[H:A ⟶ 𝕌{j}]. ∀[z:H e].  {{{False  True}}}


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] guard: {T} implies:  Q false: False true: True apply: a function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T guard: {T} implies:  Q true: True all: x:A. B[x] prop: exists: x:A. B[x]
Lemmas referenced :  istype-universe equal_wf false_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule sqequalHypSubstitution Error :lambdaEquality_alt,  dependent_functionElimination thin hypothesisEquality axiomEquality equalityTransitivity hypothesis equalitySymmetry Error :functionIsTypeImplies,  Error :inhabitedIsType,  Error :universeIsType,  applyEquality Error :isect_memberEquality_alt,  isectElimination Error :isectIsTypeImplies,  Error :functionIsType,  instantiate extract_by_obid universeEquality Error :lambdaFormation_alt,  Error :dependent_pairFormation_alt,  Error :equalityIstype,  productElimination hyp_replacement applyLambdaEquality lambdaFormation natural_numberEquality Error :equalityIsType1,  Error :setIsType,  rename setElimination Error :dependent_set_memberEquality_alt

Latex:
\mforall{}[A:Type].  \mforall{}[e:A].  \mforall{}[H:A  {}\mrightarrow{}  \mBbbU{}\{j\}].  \mforall{}[z:H  e].    \{\{\{False  {}\mRightarrow{}  True\}\}\}



Date html generated: 2019_06_20-AM-11_17_51
Last ObjectModification: 2019_03_05-PM-00_55_09

Theory : core_2


Home Index