Nuprl Lemma : bag-rep-is-single-valued
∀[A:Type]. ∀[n:ℕ]. ∀[a:A]. single-valued-bag(bag-rep(n;a);A)
Proof
Definitions occuring in Statement :
nat: ℕ,
uall: ∀[x:A]. B[x],
universe: Type,
single-valued-bag: single-valued-bag(b;T),
bag-rep: bag-rep(n;x)
Lemmas :
member-bag-rep,
bag-member_wf,
bag-rep_wf,
list-subtype-bag,
nat_wf
Latex:
\mforall{}[A:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[a:A]. single-valued-bag(bag-rep(n;a);A)
Date html generated:
2015_07_23-AM-11_25_34
Last ObjectModification:
2015_01_28-PM-11_15_31
Home
Index