### Nuprl Lemma : temp-lifting-gen-list-rev_wf

`∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[g:funtype(n - m;λx.(A (x + m));B)].`
`  (lifting-gen-list-rev(n;bags) m g ∈ bag(B))`

Proof

Definitions occuring in Statement :  lifting-gen-list-rev: `lifting-gen-list-rev(n;bags)` bag: `bag(T)` funtype: `funtype(n;A;T)` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` subtract: `n - m` add: `n + m` natural_number: `\$n` universe: `Type`
Lemmas referenced :  lifting-gen-list-rev_wf
Rules used in proof :  cut lemma_by_obid hypothesis

Latex:
\mforall{}[B:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[m:\mBbbN{}n  +  1].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[bags:k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k)].
\mforall{}[g:funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B)].
(lifting-gen-list-rev(n;bags)  m  g  \mmember{}  bag(B))

Date html generated: 2016_05_15-PM-02_59_38
Last ObjectModification: 2015_12_27-AM-09_29_18

Theory : bags

Home Index