Nuprl Lemma : finite-fun-deq_wf

[T:Type]. ∀[k:ℕ]. ∀[eq:EqDecider(T)].  (finite-fun-deq(k;eq) ∈ EqDecider(ℕk ⟶ T))


Proof




Definitions occuring in Statement :  finite-fun-deq: finite-fun-deq(k;eq) deq: EqDecider(T) int_seg: {i..j-} nat: uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] natural_number: $n universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T finite-fun-deq: finite-fun-deq(k;eq) deq: EqDecider(T) so_lambda: λ2x.t[x] nat: so_apply: x[s] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q eqof: eqof(d) rev_implies:  Q uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) uimplies: supposing a
Lemmas referenced :  bdd-all_wf int_seg_wf istype-assert deq_wf istype-nat istype-universe assert-bdd-all eqof_wf safe-assert-deq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut dependent_set_memberEquality_alt lambdaEquality_alt extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule applyEquality setElimination rename hypothesis universeIsType natural_numberEquality inhabitedIsType functionIsType lambdaFormation_alt independent_pairFormation equalityIstype because_Cache productIsType axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality_alt isectIsTypeImplies instantiate universeEquality dependent_functionElimination productElimination independent_functionElimination independent_isectElimination applyLambdaEquality functionExtensionality

Latex:
\mforall{}[T:Type].  \mforall{}[k:\mBbbN{}].  \mforall{}[eq:EqDecider(T)].    (finite-fun-deq(k;eq)  \mmember{}  EqDecider(\mBbbN{}k  {}\mrightarrow{}  T))



Date html generated: 2020_05_19-PM-09_36_35
Last ObjectModification: 2019_10_18-AM-11_58_52

Theory : equality!deciders


Home Index