Nuprl Lemma : squash_elim

[P:ℙ]. (SqStable(P)  (↓⇐⇒ P))


Proof




Definitions occuring in Statement :  sq_stable: SqStable(P) uall: [x:A]. B[x] prop: iff: ⇐⇒ Q squash: T implies:  Q
Definitions unfolded in proof :  sq_stable: SqStable(P) uall: [x:A]. B[x] implies:  Q iff: ⇐⇒ Q and: P ∧ Q member: t ∈ T prop: rev_implies:  Q squash: T
Lemmas referenced :  squash_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep Error :isect_memberFormation_alt,  lambdaFormation independent_pairFormation sqequalHypSubstitution independent_functionElimination thin hypothesis cut introduction extract_by_obid isectElimination hypothesisEquality imageMemberEquality baseClosed functionEquality Error :universeIsType,  universeEquality

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



Date html generated: 2019_06_20-AM-11_15_47
Last ObjectModification: 2018_09_26-AM-10_23_47

Theory : core_2


Home Index