---

Step * of Lemma word-equiv-equiv

∀[X:Type]. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
BY
{ (Auto THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
1. [X] : Type
2. a : (X + X) List
⊢ word-equiv(X;a;a)

2
1. [X] : Type
2. a : (X + X) List
3. b : (X + X) List
4. word-equiv(X;a;b)
⊢ word-equiv(X;b;a)

3
1. [X] : Type
2. Sym((X + X) List;w1,w2.word-equiv(X;w1;w2))
3. a : (X + X) List
4. b : (X + X) List
5. c : (X + X) List
6. word-equiv(X;a;b)
7. word-equiv(X;b;c)
⊢ word-equiv(X;a;c)

---

Latex:

---

Latex:
\mforall{}[X:Type].  EquivRel((X  +  X)  List;w1,w2.word-equiv(X;w1;w2))


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index