Nuprl Lemma : polymorphic-constant-bool

āˆ€f:ā‹‚A:Type. (A āŸ¶ š”¹). āˆƒt:š”¹. āˆ€A:Type. āˆ€x:A.  t


Proof




Definitions occuring in Statement :  bool: š”¹ all: āˆ€x:A. B[x] exists: āˆƒx:A. B[x] apply: a isect: ā‹‚x:A. B[x] function: x:A āŸ¶ B[x] universe: Type equal: t āˆˆ T
Definitions unfolded in proof :  all: āˆ€x:A. B[x] uall: āˆ€[x:A]. B[x] member: t āˆˆ T uimplies: supposing a and: P āˆ§ Q cand: cāˆ§ B bool: š”¹
Lemmas referenced :  polymorphic-constant bool_wf bool-mono union-value-type unit_wf2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis independent_isectElimination independent_pairFormation sqequalRule because_Cache dependent_functionElimination hypothesisEquality isectEquality universeEquality cumulativity functionEquality

Latex:
\mforall{}f:\mcap{}A:Type.  (A  {}\mrightarrow{}  \mBbbB{}).  \mexists{}t:\mBbbB{}.  \mforall{}A:Type.  \mforall{}x:A.    f  x  =  t



Date html generated: 2016_05_15-PM-03_15_33
Last ObjectModification: 2015_12_27-PM-01_02_55

Theory : general


Home Index