### Nuprl Lemma : implies-usquash

`∀[T:ℙ]. (T `` (∀x:Top. (x ∈ usquash(T))))`

Proof

Definitions occuring in Statement :  usquash: `usquash(T)` uall: `∀[x:A]. B[x]` top: `Top` prop: `ℙ` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` all: `∀x:A. B[x]` usquash: `usquash(T)` prop: `ℙ` uimplies: `b supposing a` so_apply: `x[s1;s2]` top: `Top`
Lemmas referenced :  top_wf pertype_wf base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalHypSubstitution hypothesis extract_by_obid hypothesisEquality sqequalRule lambdaEquality dependent_functionElimination thin axiomEquality equalityTransitivity equalitySymmetry because_Cache universeEquality pointwiseFunctionalityForEquality isectElimination independent_isectElimination applyEquality isect_memberEquality voidElimination voidEquality pertypeMemberEquality

Latex:
\mforall{}[T:\mBbbP{}].  (T  {}\mRightarrow{}  (\mforall{}x:Top.  (x  \mmember{}  usquash(T))))

Date html generated: 2019_06_20-AM-11_29_53
Last ObjectModification: 2018_09_05-PM-06_43_35

Theory : per!type!1

Home Index