Nuprl Lemma : comb_for_iff_wf

λA,B,z. (A ⇐⇒ B) ∈ A:ℙ ⟶ B:ℙ ⟶ (↓True) ⟶ ℙ


Proof




Definitions occuring in Statement :  prop: iff: ⇐⇒ Q 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 :  true_wf squash_wf iff_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalHypSubstitution imageElimination cut lemma_by_obid isectElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeEquality

Latex:
\mlambda{}A,B,z.  (A  \mLeftarrow{}{}\mRightarrow{}  B)  \mmember{}  A:\mBbbP{}  {}\mrightarrow{}  B:\mBbbP{}  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}



Date html generated: 2016_05_13-PM-03_08_11
Last ObjectModification: 2016_01_06-PM-05_27_44

Theory : core_2


Home Index