Nuprl Lemma : comb_for_grp_car_wf

λg,z. |g| ∈ g:GrpSig ⟶ (↓True) ⟶ Type


Proof




Definitions occuring in Statement :  grp_car: |g| grp_sig: GrpSig squash: T true: True member: t ∈ T lambda: λx.A[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  member: t ∈ T squash: T uall: [x:A]. B[x] prop:
Lemmas referenced :  grp_car_wf squash_wf true_wf grp_sig_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalHypSubstitution imageElimination cut lemma_by_obid isectElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry

Latex:
\mlambda{}g,z.  |g|  \mmember{}  g:GrpSig  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  Type



Date html generated: 2016_05_15-PM-00_06_28
Last ObjectModification: 2015_12_26-PM-11_47_23

Theory : groups_1


Home Index