### Nuprl Lemma : comb_for_bimplies_wf

`λp,q,z. (p ``b q) ∈ p:𝔹 ⟶ q:𝔹 supposing ↑p ⟶ (↓True) ⟶ 𝔹`

Proof

Definitions occuring in Statement :  bimplies: `p ``b q` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` squash: `↓T` true: `True` member: `t ∈ T` lambda: `λx.A[x]` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  member: `t ∈ T` squash: `↓T` uall: `∀[x:A]. B[x]` prop: `ℙ` uimplies: `b supposing a`
Lemmas referenced :  bimplies_wf squash_wf true_wf assert_wf bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaEquality_alt,  sqequalHypSubstitution imageElimination cut introduction extract_by_obid isectElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry Error :universeIsType,  sqequalRule Error :isectIsType,  Error :inhabitedIsType

Latex:
\mlambda{}p,q,z.  (p  {}\mRightarrow{}\msubb{}  q)  \mmember{}  p:\mBbbB{}  {}\mrightarrow{}  q:\mBbbB{}  supposing  \muparrow{}p  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbB{}

Date html generated: 2019_06_20-AM-11_31_15
Last ObjectModification: 2018_10_09-AM-09_29_13

Theory : bool_1

Home Index