---

Step * of Lemma squash_thru_equiv_rel

∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  ((↓EquivRel(T;x,y.E[x;y])) ⇒ EquivRel(T;x,y.↓E[x;y]))
BY
{ ((RepUnfolds ``equiv_rel refl sym trans`` 0 THEN GenUnivCD) THENA Auto) }

1
1. T : Type
2. E : T ⟶ T ⟶ ℙ
3. ↓(∀a:T. E[a;a]) ∧ (∀a,b:T.  (E[a;b] ⇒ E[b;a])) ∧ (∀a,b,c:T.  (E[a;b] ⇒ E[b;c] ⇒ E[a;c]))
4. a : T@i
⊢ ↓E[a;a]

2
1. T : Type
2. E : T ⟶ T ⟶ ℙ
3. ↓(∀a:T. E[a;a]) ∧ (∀a,b:T.  (E[a;b] ⇒ E[b;a])) ∧ (∀a,b,c:T.  (E[a;b] ⇒ E[b;c] ⇒ E[a;c]))
4. a : T@i
5. b : T@i
6. ↓E[a;b]
⊢ ↓E[b;a]

3
1. T : Type
2. E : T ⟶ T ⟶ ℙ
3. ↓(∀a:T. E[a;a]) ∧ (∀a,b:T.  (E[a;b] ⇒ E[b;a])) ∧ (∀a,b,c:T.  (E[a;b] ⇒ E[b;c] ⇒ E[a;c]))
4. a : T@i
5. b : T@i
6. c : T@i
7. ↓E[a;b]
8. ↓E[b;c]
⊢ ↓E[a;c]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    ((\mdownarrow{}EquivRel(T;x,y.E[x;y]))  {}\mRightarrow{}  EquivRel(T;x,y.\mdownarrow{}E[x;y]))


By

---

Latex:
((RepUnfolds  ``equiv\_rel  refl  sym  trans``  0  THEN  GenUnivCD)  THENA  Auto)

---

Home Index