Nuprl Lemma : concat-lifting-loc-1_wf

[B,A:Type]. ∀[f:Id ─→ A ─→ bag(B)].  (f@ ∈ Id ─→ bag(A) ─→ bag(B))


Proof




Definitions occuring in Statement :  concat-lifting-loc-1: f@ Id: Id uall: [x:A]. B[x] member: t ∈ T function: x:A ─→ B[x] universe: Type bag: bag(T)
Lemmas :  concat-lifting1-loc_wf bag_wf Id_wf

Latex:
\mforall{}[B,A:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  bag(B)].    (f@  \mmember{}  Id  {}\mrightarrow{}  bag(A)  {}\mrightarrow{}  bag(B))



Date html generated: 2015_07_22-PM-00_08_11
Last ObjectModification: 2015_01_28-AM-11_41_52

Home Index