---

Step * 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. x1 (λx,y. ((R x y) ∨ (R y x))) y1
12. P[x1]
⊢ P[y1]
BY
{ (RepUR ``infix_ap`` -2 THEN D -2) }

1
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]

2
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 y1 x1
12. P[x1]
⊢ P[y1]

---

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.  x1  (\mlambda{}x,y.  ((R  x  y)  \mvee{}  (R  y  x)))  y1
12.  P[x1]
\mvdash{}  P[y1]


By

---

Latex:
(RepUR  ``infix\_ap``  -2  THEN  D  -2)

---

Home Index