---

Step * of Lemma equiv_rel_quotient

∀[T:Type]. ∀[E1,E2:T ⟶ T ⟶ 𝔹].
  (EquivRel(T;x,y.↑E2[x;y])
  ⇒ EquivRel(T;x,y.↑E1[x;y])
  ⇒ (∀x,y:T.  ((↑E2[x;y]) ⇒ (↑E1[x;y])))
  ⇒ EquivRel(x,y:T//(↑E2[x;y]);x,y.↑E1[x;y]))
BY
{ ((BasicUniformUnivCD Auto THEN RepeatFor 3 ((D 0 THENA Auto)))
   THEN (InstLemma `equiv_rel-wf-quotient` [⌜T⌝;⌜E1⌝;⌜E2⌝]⋅ THENA Auto)
   THEN RepeatFor 2 ((D 0 THEN Auto))) }

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

2
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])
9. b : x,y:T//(↑E2[x;y])
10. ↑E1[a;b]
⊢ ↑E1[b;a]

3
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. Sym(x,y:T//(↑E2[x;y]);x,y.↑E1[x;y])
9. a : x,y:T//(↑E2[x;y])
10. b : x,y:T//(↑E2[x;y])
11. c : x,y:T//(↑E2[x;y])
12. ↑E1[a;b]
13. ↑E1[b;c]
⊢ ↑E1[a;c]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[E1,E2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].
    (EquivRel(T;x,y.\muparrow{}E2[x;y])
    {}\mRightarrow{}  EquivRel(T;x,y.\muparrow{}E1[x;y])
    {}\mRightarrow{}  (\mforall{}x,y:T.    ((\muparrow{}E2[x;y])  {}\mRightarrow{}  (\muparrow{}E1[x;y])))
    {}\mRightarrow{}  EquivRel(x,y:T//(\muparrow{}E2[x;y]);x,y.\muparrow{}E1[x;y]))


By

---

Latex:
((BasicUniformUnivCD  Auto  THEN  RepeatFor  3  ((D  0  THENA  Auto)))
  THEN  (InstLemma  `equiv\_rel-wf-quotient`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}E1\mkleeneclose{};\mkleeneopen{}E2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index