---

Step * of Lemma equiv-class_wf

∀[A:Type]. ∀[E:A ⟶ A ⟶ 𝔹].
  ∀[t:x,y:A//(↑E[x;y])]. (equiv-class(A;x,y.E[x;y];t) ∈ Type) supposing EquivRel(A;x,y.↑E[x;y])
BY
{ (Auto THEN D -1 THEN Unfold `equiv-class` 0 THEN RepeatFor 2 (EqCDA)) }

1
.....subterm..... T:t
1:n
1. A : Type
2. E : A ⟶ A ⟶ 𝔹
3. EquivRel(A;x,y.↑E[x;y])
4. t : Base
5. t1 : Base
6. t = t1 ∈ pertype(λx,y. ((x ∈ A) ∧ (y ∈ A) ∧ (↑E[x;y])))
7. t ∈ A
8. t1 ∈ A
9. ↑E[t;t1]
10. y : A
⊢ E[t;y] = E[t1;y]

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}].
    \mforall{}[t:x,y:A//(\muparrow{}E[x;y])].  (equiv-class(A;x,y.E[x;y];t)  \mmember{}  Type)  supposing  EquivRel(A;x,y.\muparrow{}E[x;y])


By

---

Latex:
(Auto  THEN  D  -1  THEN  Unfold  `equiv-class`  0  THEN  RepeatFor  2  (EqCDA))

---

Home Index