---

Step * of Lemma type-equating-some

∀T:Type. ∀P:T ⟶ ℙ.
  ∃T':Type
   ((T ⊆r T') ∧ (∀x,y:T.  (P[x] ⇒ P[y] ⇒ (x = y ∈ T'))) ∧ (∀x,y:T.  ((¬P[x]) ⇒ (x = y ∈ T ⇐⇒ x = y ∈ T'))))
BY
{ (Auto
   THEN D 0 With ⌜x,y:T//(least-equiv(T;λx,y. (P[x] ∧ P[y])) x y)⌝ 
   THEN Auto
   THEN Try (((EqTypeCD THEN Auto) THEN InstLemma  `implies-least-equiv` [⌜T⌝;⌜λx,y. (P[x] ∧ P[y])⌝]⋅ THEN Auto))
   THEN EqTypeHD (-1)
   ⋅
   THEN Auto) }

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. least-equiv(T;λx,y. (P[x] ∧ P[y])) x y
⊢ x = y ∈ T

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}P:T  {}\mrightarrow{}  \mBbbP{}.
    \mexists{}T':Type
      ((T  \msubseteq{}r  T')  \mwedge{}  (\mforall{}x,y:T.    (P[x]  {}\mRightarrow{}  P[y]  {}\mRightarrow{}  (x  =  y)))  \mwedge{}  (\mforall{}x,y:T.    ((\mneg{}P[x])  {}\mRightarrow{}  (x  =  y  \mLeftarrow{}{}\mRightarrow{}  x  =  y))))


By

---

Latex:
(Auto
  THEN  D  0  With  \mkleeneopen{}x,y:T//(least-equiv(T;\mlambda{}x,y.  (P[x]  \mwedge{}  P[y]))  x  y)\mkleeneclose{} 
  THEN  Auto
  THEN  Try  (((EqTypeCD  THEN  Auto)
                        THEN  InstLemma    `implies-least-equiv`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  (P[x]  \mwedge{}  P[y])\mkleeneclose{}]\mcdot{}
                        THEN  Auto))
  THEN  EqTypeHD  (-1)
  \mcdot{}
  THEN  Auto)

---

Home Index