Nuprl Lemma : fresh-cname-not-equal

I:Cname List. ∀[x:nameset(I)]. (fresh-cname(I) x ∈ Cname))


Proof




Definitions occuring in Statement :  fresh-cname: fresh-cname(I) nameset: nameset(L) coordinate_name: Cname list: List uall: [x:A]. B[x] all: x:A. B[x] not: ¬A equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T not: ¬A implies:  Q false: False so_lambda: λ2x.t[x] prop: so_apply: x[s] subtype_rel: A ⊆B nameset: nameset(L) uimplies: supposing a coordinate_name: Cname int_upper: {i...} sq_type: SQType(T) guard: {T}
Lemmas referenced :  fresh-cname_wf set_wf coordinate_name_wf not_wf l_member_wf equal_wf nameset_wf list_wf subtype_base_sq set_subtype_base le_wf int_subtype_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis sqequalRule lambdaEquality equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination voidElimination applyEquality setElimination rename setEquality because_Cache instantiate cumulativity independent_isectElimination intEquality natural_numberEquality

Latex:
\mforall{}I:Cname  List.  \mforall{}[x:nameset(I)].  (\mneg{}(fresh-cname(I)  =  x))



Date html generated: 2017_10_05-AM-10_05_09
Last ObjectModification: 2017_07_28-AM-11_15_57

Theory : cubical!sets


Home Index