### Nuprl Lemma : fpf-join-list_wf

`∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[L:a:A fp-> B[a] List].  (⊕(L) ∈ a:A fp-> B[a])`

Proof

Definitions occuring in Statement :  fpf-join-list: `⊕(L)` fpf: `a:A fp-> B[a]` list: `T List` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  fpf-join-list: `⊕(L)` uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  reduce_wf fpf_wf fpf-join_wf fpf-empty_wf list_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality applyEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache functionEquality cumulativity universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[L:a:A  fp->  B[a]  List].    (\moplus{}(L)  \mmember{}  a:A  fp->  B[a])

Date html generated: 2018_05_21-PM-09_22_37
Last ObjectModification: 2018_02_09-AM-10_18_49

Theory : finite!partial!functions

Home Index