Nuprl Lemma : squash-test

[P:ℙ]. (P  (↓P))


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: squash: T implies:  Q
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q squash: T prop:
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation hypothesis sqequalRule imageMemberEquality hypothesisEquality thin baseClosed sqequalHypSubstitution imageElimination lambdaEquality dependent_functionElimination universeEquality

Latex:
\mforall{}[P:\mBbbP{}].  (P  {}\mRightarrow{}  (\mdownarrow{}P))



Date html generated: 2016_05_13-PM-03_07_57
Last ObjectModification: 2016_01_06-PM-05_48_04

Theory : core_2


Home Index