---

Step * 3 1 of Lemma length-one-iff


1. T : Type
2. u : T
3. u1 : T
4. v : T List
5. ∀[x,y:T].  (x = y ∈ T) supposing ((y ∈ [u; [u1 / v]]) and (x ∈ [u; [u1 / v]]))
6. no_repeats(T;[u; [u1 / v]])
7. 0 < (||v|| + 1) + 1
⊢ ((||v|| + 1) + 1) = 1 ∈ ℤ
BY
{ (RWO "no_repeats_cons" (-2) THEN Auto THEN D -2) }

1
1. T : Type
2. u : T
3. u1 : T
4. v : T List
5. ∀[x,y:T].  (x = y ∈ T) supposing ((y ∈ [u; [u1 / v]]) and (x ∈ [u; [u1 / v]]))
6. no_repeats(T;[u1 / v])
7. 0 < (||v|| + 1) + 1
⊢ (u ∈ [u1 / v])

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  u1  :  T
4.  v  :  T  List
5.  \mforall{}[x,y:T].    (x  =  y)  supposing  ((y  \mmember{}  [u;  [u1  /  v]])  and  (x  \mmember{}  [u;  [u1  /  v]]))
6.  no\_repeats(T;[u;  [u1  /  v]])
7.  0  <  (||v||  +  1)  +  1
\mvdash{}  ((||v||  +  1)  +  1)  =  1


By

---

Latex:
(RWO  "no\_repeats\_cons"  (-2)  THEN  Auto  THEN  D  -2)

---

Home Index