### Nuprl Lemma : lift-predicate_wf

`∀[A:Type]. ∀[P:A ⟶ ℙ].  P? ∈ bar(A) ⟶ ℙ supposing value-type(A)`

Proof

Definitions occuring in Statement :  lift-predicate: `P?` bar: `bar(T)` value-type: `value-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` lift-predicate: `P?` implies: `P `` Q` prop: `ℙ` subtype_rel: `A ⊆r B` bar: `bar(T)`
Lemmas referenced :  termination value-type_wf bar_wf has-value_wf-bar
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality functionEquality lemma_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality independent_isectElimination hypothesis applyEquality universeEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].    P?  \mmember{}  bar(A)  {}\mrightarrow{}  \mBbbP{}  supposing  value-type(A)

Date html generated: 2016_05_15-PM-10_04_26
Last ObjectModification: 2016_01_05-PM-06_50_55

Theory : bar!type

Home Index