### Nuprl Lemma : quotient-implies-squash

`∀[P,Q:ℙ].  ((P `` Q) `` {⇃(P) `` (↓Q)})`

Proof

Definitions occuring in Statement :  quotient: `x,y:A//B[x; y]` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` squash: `↓T` implies: `P `` Q` true: `True`
Definitions unfolded in proof :  guard: `{T}` uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` prop: `ℙ` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` squash: `↓T` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a`
Lemmas referenced :  equiv_rel_true quotient_wf true_wf equal-wf-base squash_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lambdaFormation rename pointwiseFunctionalityForEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis pertypeElimination productElimination independent_functionElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed productEquality because_Cache imageElimination cumulativity lambdaEquality independent_isectElimination functionEquality dependent_functionElimination universeEquality isect_memberEquality

Latex:
\mforall{}[P,Q:\mBbbP{}].    ((P  {}\mRightarrow{}  Q)  {}\mRightarrow{}  \{\00D9(P)  {}\mRightarrow{}  (\mdownarrow{}Q)\})

Date html generated: 2016_05_19-AM-11_56_56
Last ObjectModification: 2016_05_18-AM-08_21_36

Theory : quot_1

Home Index