---

Step * 1 of Lemma type-equating-some


1. T : Type
2. P : T ⟶ ℙ
3. T ⊆r (x,y:T//(least-equiv(T;λx,y. (P[x] ∧ P[y])) x y))
4. ∀x,y:T.  (P[x] ⇒ P[y] ⇒ (x = y ∈ (x,y:T//(least-equiv(T;λx,y. (P[x] ∧ P[y])) x y))))
5. x : T
6. y : T
7. ¬P[x]
8. x = y ∈ pertype(λx,y. ((x ∈ T) ∧ (y ∈ T) ∧ (least-equiv(T;λx,y. (P[x] ∧ P[y])) x y)))
9. x ∈ T
10. y ∈ T
11. least-equiv(T;λx,y. (P[x] ∧ P[y])) x y
⊢ x = y ∈ T
BY
{ (RepUR ``least-equiv transitive-reflexive-closure`` -1 THEN D -1 THEN Try (Trivial)) }

1
1. T : Type
2. P : T ⟶ ℙ
3. T ⊆r (x,y:T//(least-equiv(T;λx,y. (P[x] ∧ P[y])) x y))
4. ∀x,y:T.  (P[x] ⇒ P[y] ⇒ (x = y ∈ (x,y:T//(least-equiv(T;λx,y. (P[x] ∧ P[y])) x y))))
5. x : T
6. y : T
7. ¬P[x]
8. x = y ∈ pertype(λx,y. ((x ∈ T) ∧ (y ∈ T) ∧ (least-equiv(T;λx,y. (P[x] ∧ P[y])) x y)))
9. x ∈ T
10. y ∈ T
11. TC(λx,y. ((P[x] ∧ P[y]) ∨ (P[y] ∧ P[x]))) x y
⊢ x = y ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbP{}
3.  T  \msubseteq{}r  (x,y:T//(least-equiv(T;\mlambda{}x,y.  (P[x]  \mwedge{}  P[y]))  x  y))
4.  \mforall{}x,y:T.    (P[x]  {}\mRightarrow{}  P[y]  {}\mRightarrow{}  (x  =  y))
5.  x  :  T
6.  y  :  T
7.  \mneg{}P[x]
8.  x  =  y
9.  x  \mmember{}  T
10.  y  \mmember{}  T
11.  least-equiv(T;\mlambda{}x,y.  (P[x]  \mwedge{}  P[y]))  x  y
\mvdash{}  x  =  y


By

---

Latex:
(RepUR  ``least-equiv  transitive-reflexive-closure``  -1  THEN  D  -1  THEN  Try  (Trivial))

---

Home Index