### Nuprl Lemma : not-not-sig-to-W

`∀A:Type. ∀B:A ⟶ Type.  ((∀R:Type. (((a:A × (B[a] `` R)) `` R) `` R)) `` W(A;a.B[a]))`

Proof

Definitions occuring in Statement :  W: `W(A;a.B[a])` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` product: `x:A × B[x]` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_apply: `x[s]` so_lambda: `λ2x.t[x]` ext-eq: `A ≡ B` and: `P ∧ Q` subtype_rel: `A ⊆r B`
Lemmas referenced :  istype-universe W_wf W-ext
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  sqequalRule Error :functionIsType,  Error :inhabitedIsType,  hypothesisEquality Error :productIsType,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis Error :universeIsType,  applyEquality universeEquality dependent_functionElimination Error :lambdaEquality_alt,  independent_functionElimination because_Cache rename productElimination

Latex:
\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.    ((\mforall{}R:Type.  (((a:A  \mtimes{}  (B[a]  {}\mRightarrow{}  R))  {}\mRightarrow{}  R)  {}\mRightarrow{}  R))  {}\mRightarrow{}  W(A;a.B[a]))

Date html generated: 2019_06_20-PM-00_36_41
Last ObjectModification: 2018_10_06-AM-11_20_24

Theory : co-recursion

Home Index