---

Step * 2 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])
9. b : x,y:T//(↑E2[x;y])
⊢ λx.Ax ∈ (↑E1[a;b]) ⇒ (↑E1[b;a])
BY
{ ((DVar `a' THEN Try (Complete (Auto)))
   THEN DVar `b'
   THEN Auto
   THEN RepeatFor 2 (EqCD)
   THEN Auto
   THEN BLemma `iff_imp_equal_bool`
   THEN Auto
   THEN Try ((Complete (UseTrans ⌜y⌝⋅) ORELSE Complete (UseTrans ⌜x⌝⋅)))) }

---

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])
9.  b  :  x,y:T//(\muparrow{}E2[x;y])
\mvdash{}  \mlambda{}x.Ax  \mmember{}  (\muparrow{}E1[a;b])  {}\mRightarrow{}  (\muparrow{}E1[b;a])


By

---

Latex:
((DVar  `a'  THEN  Try  (Complete  (Auto)))
  THEN  DVar  `b'
  THEN  Auto
  THEN  RepeatFor  2  (EqCD)
  THEN  Auto
  THEN  BLemma  `iff\_imp\_equal\_bool`
  THEN  Auto
  THEN  Try  ((Complete  (UseTrans  \mkleeneopen{}y\mkleeneclose{}\mcdot{})  ORELSE  Complete  (UseTrans  \mkleeneopen{}x\mkleeneclose{}\mcdot{}))))

---

Home Index