### Nuprl Lemma : double-negation-iff-xmiddle

`∀[A:Type]. (∀[P:ℙ]. (((P `` A) `` A) `` (P ∨ A)) `⇐⇒` ∀[P:ℙ]. (P ∨ (P `` A)))`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` prop: `ℙ` iff: `P `⇐⇒` Q` implies: `P `` Q` or: `P ∨ Q` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` rev_implies: `P `` Q` or: `P ∨ Q` guard: `{T}`
Lemmas referenced :  uall_wf or_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation independent_pairFormation lambdaFormation universeEquality cut thin instantiate lemma_by_obid sqequalHypSubstitution isectElimination sqequalRule lambdaEquality cumulativity functionEquality hypothesisEquality hypothesis independent_functionElimination inrFormation inlFormation because_Cache unionElimination

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

Date html generated: 2016_05_15-PM-03_19_06
Last ObjectModification: 2015_12_27-PM-01_03_47

Theory : general

Home Index