Nuprl Lemma : minimal-not-not-excluded-middle-ext

[A,P:ℙ].  (((P ∨ (P  A))  A)  A)


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: implies:  Q or: P ∨ Q
Definitions unfolded in proof :  member: t ∈ T minimal-not-not-excluded-middle
Lemmas referenced :  minimal-not-not-excluded-middle
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

Latex:
\mforall{}[A,P:\mBbbP{}].    (((P  \mvee{}  (P  {}\mRightarrow{}  A))  {}\mRightarrow{}  A)  {}\mRightarrow{}  A)



Date html generated: 2018_05_21-PM-00_02_24
Last ObjectModification: 2018_05_19-AM-07_11_20

Theory : call!by!value_2


Home Index