Nuprl Lemma : add-fresh-cname_wf

[I:Cname List]. (I+ ∈ Cname List)


Proof




Definitions occuring in Statement :  add-fresh-cname: I+ coordinate_name: Cname list: List uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T add-fresh-cname: I+ has-value: (a)↓ prop: uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B
Lemmas referenced :  value-type-has-value coordinate_name_wf not_wf l_member_wf set-value-type coordinate_name-value-type fresh-cname_wf cons_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule callbyvalueReduce lemma_by_obid sqequalHypSubstitution isectElimination thin setEquality hypothesis hypothesisEquality independent_isectElimination lambdaEquality applyEquality setElimination rename axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[I:Cname  List].  (I+  \mmember{}  Cname  List)



Date html generated: 2016_05_20-AM-09_28_52
Last ObjectModification: 2015_12_28-PM-04_48_00

Theory : cubical!sets


Home Index