---

Step * 1 of Lemma single-valued-bag-hd


1. T : Type
2. T List ∈ Type
3. ∀as,bs:T List.  (permutation(T;as;bs) ∈ Type)
4. ∀as:T List. permutation(T;as;as)
5. a : Base
6. b1 : Base
7. c : a = b1 ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
8. a ∈ T List
9. b1 ∈ T List
10. permutation(T;a;b1)
11. single-valued-bag(a;T)
12. 0 < ||a||
⊢ hd(a) = hd(b1) ∈ T
BY
{ ((FLemma `permutation-length` [-3] THENA Auto)
   THEN Unfold `permutation` (-4)
   THEN ExRepD
   THEN (HypSubst' (-4) 0 THENA Auto)
   THEN ThinVar `b1'
   THEN (RWO "select0<" 0 THENA Auto)
   THEN (RWO "permute_list_select" 0 THENA Auto)
   THEN Unfold `single-valued-bag` (-2)
   THEN InstHyp [⌜a[0]⌝;⌜a[f 0]⌝] (-2)⋅
   THEN Auto'
   THEN (BLemma `list-member-bag-member` THENA Auto')
   THEN GenListD 0)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  T  List  \mmember{}  Type
3.  \mforall{}as,bs:T  List.    (permutation(T;as;bs)  \mmember{}  Type)
4.  \mforall{}as:T  List.  permutation(T;as;as)
5.  a  :  Base
6.  b1  :  Base
7.  c  :  a  =  b1
8.  a  \mmember{}  T  List
9.  b1  \mmember{}  T  List
10.  permutation(T;a;b1)
11.  single-valued-bag(a;T)
12.  0  <  ||a||
\mvdash{}  hd(a)  =  hd(b1)


By

---

Latex:
((FLemma  `permutation-length`  [-3]  THENA  Auto)
  THEN  Unfold  `permutation`  (-4)
  THEN  ExRepD
  THEN  (HypSubst'  (-4)  0  THENA  Auto)
  THEN  ThinVar  `b1'
  THEN  (RWO  "select0<"  0  THENA  Auto)
  THEN  (RWO  "permute\_list\_select"  0  THENA  Auto)
  THEN  Unfold  `single-valued-bag`  (-2)
  THEN  InstHyp  [\mkleeneopen{}a[0]\mkleeneclose{};\mkleeneopen{}a[f  0]\mkleeneclose{}]  (-2)\mcdot{}
  THEN  Auto'
  THEN  (BLemma  `list-member-bag-member`  THENA  Auto')
  THEN  GenListD  0)\mcdot{}

---

Home Index