---

Step * of Lemma transitive-reflexive-closure-base-case

∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  ∀x,y:A.  ((x R y) ⇒ (x R^* y))
BY
{ (Auto THEN RepUR ``transitive-reflexive-closure`` 0 THEN OrRight THEN Auto) }

1
1. [A] : Type
2. [R] : A ⟶ A ⟶ ℙ
3. x : A
4. y : A
5. x R y
⊢ TC(R) x y

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,y:A.    ((x  R  y)  {}\mRightarrow{}  (x  R\^{}*  y))


By

---

Latex:
(Auto  THEN  RepUR  ``transitive-reflexive-closure``  0  THEN  OrRight  THEN  Auto)

---

Home Index