Nuprl Lemma : half-squash-stable_wf

[P:ℙ]. (half-squash-stable(P) ∈ ℙ)


Proof




Definitions occuring in Statement :  half-squash-stable: half-squash-stable(P) uall: [x:A]. B[x] prop: member: t ∈ T
Definitions unfolded in proof :  uimplies: supposing a so_apply: x[s1;s2] so_lambda: λ2y.t[x; y] prop: implies:  Q half-squash-stable: half-squash-stable(P) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  equiv_rel_true true_wf quotient_wf
Rules used in proof :  universeEquality equalitySymmetry equalityTransitivity axiomEquality independent_isectElimination because_Cache hypothesis lambdaEquality hypothesisEquality cumulativity thin isectElimination sqequalHypSubstitution extract_by_obid functionEquality sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[P:\mBbbP{}].  (half-squash-stable(P)  \mmember{}  \mBbbP{})



Date html generated: 2017_09_29-PM-05_48_09
Last ObjectModification: 2017_08_30-AM-10_28_59

Theory : quot_1


Home Index