---

Step * 1 of Lemma transmem_transitivity


1. UniformlyTrans(coSet{i:l};x,y.x TC(λx,y. (x ∈ y)) y)
⊢ Trans(coSet{i:l};x,y.x TC(λx,y. (x ∈ y)) y)
BY
{ ((UnfoldTopAb (-1) THEN UnfoldTopAb 0) THEN RepeatFor 3 (ParallelLast)) }

---

Latex:

---

Latex:

1.  UniformlyTrans(coSet\{i:l\};x,y.x  TC(\mlambda{}x,y.  (x  \mmember{}  y))  y)
\mvdash{}  Trans(coSet\{i:l\};x,y.x  TC(\mlambda{}x,y.  (x  \mmember{}  y))  y)


By

---

Latex:
((UnfoldTopAb  (-1)  THEN  UnfoldTopAb  0)  THEN  RepeatFor  3  (ParallelLast))

---

Home Index