Nuprl Lemma : comb_for_band_wf

λp,q,z. (p ∧b q) ∈ p:𝔹 ⟶ q:𝔹 ⟶ (↓True) ⟶ 𝔹


Proof




Definitions occuring in Statement :  band: p ∧b q bool: 𝔹 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:
Lemmas referenced :  band_wf squash_wf true_wf bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalHypSubstitution imageElimination cut lemma_by_obid isectElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry

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



Date html generated: 2016_05_13-PM-03_56_02
Last ObjectModification: 2015_12_26-AM-10_52_46

Theory : bool_1


Home Index