---

Step * 1 1 of Lemma least-equiv-induction


1. [A] : Type
2. [P] : A ⟶ ℙ
3. [R] : A ⟶ A ⟶ ℙ
4. ∀x,y:A.  ((R x y) ⇒ (P[x] ⇐⇒ P[y]))
5. x : A
6. y : A
7. TC(λx,y. ((R x y) ∨ (R y x))) x y
8. P[x]
9. x1 : A
10. y1 : A
11. R x1 y1
12. P[x1]
⊢ P[y1]
BY
{ (InstHyp [⌜x1⌝;⌜y1⌝] 4⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [P]  :  A  {}\mrightarrow{}  \mBbbP{}
3.  [R]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x,y:A.    ((R  x  y)  {}\mRightarrow{}  (P[x]  \mLeftarrow{}{}\mRightarrow{}  P[y]))
5.  x  :  A
6.  y  :  A
7.  TC(\mlambda{}x,y.  ((R  x  y)  \mvee{}  (R  y  x)))  x  y
8.  P[x]
9.  x1  :  A
10.  y1  :  A
11.  R  x1  y1
12.  P[x1]
\mvdash{}  P[y1]


By

---

Latex:
(InstHyp  [\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}y1\mkleeneclose{}]  4\mcdot{}  THEN  Auto)

---

Home Index