Nuprl Lemma : page55'

[U:Type]. ∀[P,Q:U ⟶ ℙ].  ∀f:∀x:U. (P[x]  Q[x]). ∀g:∀x:U. P[x]. ∀x:U.  Q[x]


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T prop: so_lambda: λ2x.t[x] so_apply: x[s] implies:  Q
Lemmas referenced :  all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation hypothesisEquality cut lemma_by_obid sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality applyEquality hypothesis functionEquality cumulativity universeEquality dependent_functionElimination independent_functionElimination

Latex:
\mforall{}[U:Type].  \mforall{}[P,Q:U  {}\mrightarrow{}  \mBbbP{}].    \mforall{}f:\mforall{}x:U.  (P[x]  {}\mRightarrow{}  Q[x]).  \mforall{}g:\mforall{}x:U.  P[x].  \mforall{}x:U.    Q[x]



Date html generated: 2016_05_15-PM-07_42_35
Last ObjectModification: 2015_12_27-AM-11_13_07

Theory : general


Home Index