---

Step * 1 2 1 of Lemma rel_exp-iff-path


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. x : T@i
4. y : T@i
5. u : T
6. 1 = 1 ∈ ℤ
7. rel-path-between(T;R;x;y;[u])
⊢ x = y ∈ T
BY
{ ((D (-1)⋅ THEN RepUR ``last`` -1) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  x  :  T@i
4.  y  :  T@i
5.  u  :  T
6.  1  =  1
7.  rel-path-between(T;R;x;y;[u])
\mvdash{}  x  =  y


By

---

Latex:
((D  (-1)\mcdot{}  THEN  RepUR  ``last``  -1)  THEN  Auto)

---

Home Index