---

Step * 1 of Lemma equiv_rel_quotient


1. [T] : Type
2. [E1] : T ⟶ T ⟶ 𝔹
3. [E2] : T ⟶ T ⟶ 𝔹
4. EquivRel(T;x,y.↑E2[x;y])
5. EquivRel(T;x,y.↑E1[x;y])
6. ∀x,y:T.  ((↑E2[x;y]) ⇒ (↑E1[x;y]))
7. E1 ∈ (x,y:T//(↑E2[x;y])) ⟶ (x,y:T//(↑E2[x;y])) ⟶ 𝔹
8. a : x,y:T//(↑E2[x;y])
⊢ ↑E1[a;a]
BY
{ (UseWitness ⌜Ax⌝⋅ THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [E1]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
3.  [E2]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
4.  EquivRel(T;x,y.\muparrow{}E2[x;y])
5.  EquivRel(T;x,y.\muparrow{}E1[x;y])
6.  \mforall{}x,y:T.    ((\muparrow{}E2[x;y])  {}\mRightarrow{}  (\muparrow{}E1[x;y]))
7.  E1  \mmember{}  (x,y:T//(\muparrow{}E2[x;y]))  {}\mrightarrow{}  (x,y:T//(\muparrow{}E2[x;y]))  {}\mrightarrow{}  \mBbbB{}
8.  a  :  x,y:T//(\muparrow{}E2[x;y])
\mvdash{}  \muparrow{}E1[a;a]


By

---

Latex:
(UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  D  -1  THEN  Auto)

---

Home Index