### Nuprl Lemma : half-squash-stable__and

`∀[P,Q:ℙ].  (half-squash-stable(P) `` half-squash-stable(Q) `` half-squash-stable(P ∧ Q))`

Proof

Definitions occuring in Statement :  half-squash-stable: `half-squash-stable(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` implies: `P `` Q` and: `P ∧ Q`
Definitions unfolded in proof :  guard: `{T}` uimplies: `b supposing a` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` prop: `ℙ` member: `t ∈ T` cand: `A c∧ B` and: `P ∧ Q` implies: `P `` Q` uall: `∀[x:A]. B[x]` half-squash-stable: `half-squash-stable(P)`
Lemmas referenced :  implies-quotient-true equiv_rel_true true_wf quotient_wf
Rules used in proof :  promote_hyp independent_functionElimination productElimination universeEquality functionEquality independent_isectElimination because_Cache lambdaEquality hypothesisEquality cumulativity productEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction hypothesis independent_pairFormation cut lambdaFormation isect_memberFormation computationStep sqequalTransitivity sqequalReflexivity sqequalRule sqequalSubstitution

Latex:
\mforall{}[P,Q:\mBbbP{}].    (half-squash-stable(P)  {}\mRightarrow{}  half-squash-stable(Q)  {}\mRightarrow{}  half-squash-stable(P  \mwedge{}  Q))

Date html generated: 2017_09_29-PM-05_48_10
Last ObjectModification: 2017_08_30-AM-11_07_04

Theory : quot_1

Home Index