Nuprl Lemma : comb_for_assoced_wf

λa,b,z. (a b) ∈ a:ℤ ⟶ b:ℤ ⟶ (↓True) ⟶ ℙ


Proof




Definitions occuring in Statement :  assoced: b prop: squash: T true: True member: t ∈ T lambda: λx.A[x] function: x:A ⟶ B[x] int:
Definitions unfolded in proof :  member: t ∈ T squash: T uall: [x:A]. B[x] prop:
Lemmas referenced :  assoced_wf squash_wf true_wf istype-int
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,  Error :inhabitedIsType

Latex:
\mlambda{}a,b,z.  (a  \msim{}  b)  \mmember{}  a:\mBbbZ{}  {}\mrightarrow{}  b:\mBbbZ{}  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}



Date html generated: 2019_06_20-PM-02_20_46
Last ObjectModification: 2018_10_03-AM-00_35_47

Theory : num_thy_1


Home Index