---

Step * 2 of Lemma length-one-iff


1. T : Type
2. L : T List
3. ||L|| = 1 ∈ ℤ
⊢ no_repeats(T;L)
BY
{ (DVar `L' THEN All Reduce THEN Auto THEN DVar `v' THEN All Reduce THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  ||L||  =  1
\mvdash{}  no\_repeats(T;L)


By

---

Latex:
(DVar  `L'  THEN  All  Reduce  THEN  Auto  THEN  DVar  `v'  THEN  All  Reduce  THEN  Auto')

---

Home Index