Nuprl Lemma : nc-0_wf

[I:fset(ℕ)]. ∀[i:ℕ].  ((i0) ∈ I ⟶ I+i)


Proof




Definitions occuring in Statement :  nc-0: (i0) add-name: I+i names-hom: I ⟶ J fset: fset(T) nat: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  names-hom: I ⟶ J uall: [x:A]. B[x] member: t ∈ T nc-0: (i0) names: names(I) nat: all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a top: Top bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False
Lemmas referenced :  eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int dM0-sq-empty dM0_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int dM_inc_wf not-added-name names_wf add-name_wf nat_wf fset_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lambdaEquality extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename because_Cache hypothesis lambdaFormation unionElimination equalityElimination productElimination independent_isectElimination isect_memberEquality voidElimination voidEquality hypothesisEquality equalityTransitivity equalitySymmetry dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination axiomEquality

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\mBbbN{}].    ((i0)  \mmember{}  I  {}\mrightarrow{}  I+i)



Date html generated: 2017_10_05-AM-01_02_16
Last ObjectModification: 2017_07_28-AM-09_26_12

Theory : cubical!type!theory


Home Index