Nuprl Lemma : permutation-sv-list
∀[A:Type]. ∀[L1,L2:A List]. (single-valued-list(L1;A) ⇒ permutation(A;L1;L2) ⇒ (L1 = L2 ∈ (A List)))
Proof
Definitions occuring in Statement :
single-valued-list: single-valued-list(L;T),
permutation: permutation(T;L1;L2),
list: T List,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
universe: Type,
equal: s = t ∈ T
Lemmas :
list_extensionality,
less_than_wf,
length_wf,
nat_wf,
length_wf_nat,
equal_wf,
permute_list_length,
select_wf,
sq_stable__le,
select_member,
lelt_wf,
l_member_wf,
squash_wf,
true_wf,
permute_list_select,
iff_weakening_equal,
le_wf,
list_wf
Latex:
\mforall{}[A:Type]. \mforall{}[L1,L2:A List]. (single-valued-list(L1;A) {}\mRightarrow{} permutation(A;L1;L2) {}\mRightarrow{} (L1 = L2))
Date html generated:
2015_07_23-AM-11_25_57
Last ObjectModification:
2015_02_04-PM-04_45_52
Home
Index