---

Step * 1 of Lemma finite-quotient


1. A : Type
2. R : A ⟶ A ⟶ ℙ
3. L : A List
4. no_repeats(A;L)
5. ∀x:A. (x ∈ L)
6. EquivRel(A;x,y.x R y)
7. ∀x,y:A.  Dec(x R y)
⊢ ∃L:(x,y:A//(x R y)) List. (no_repeats(x,y:A//(x R y);L) ∧ (∀x:x,y:A//(x R y). (x ∈ L)))
BY
{ (InstLemma `decidable__quotient_equal` [⌜A⌝;⌜R⌝]⋅ THENA Auto) }

1
1. A : Type
2. R : A ⟶ A ⟶ ℙ
3. L : A List
4. no_repeats(A;L)
5. ∀x:A. (x ∈ L)
6. EquivRel(A;x,y.x R y)
7. ∀x,y:A.  Dec(x R y)
8. ∀u,v:x,y:A//R[x;y].  Dec(u = v ∈ (x,y:A//R[x;y]))
⊢ ∃L:(x,y:A//(x R y)) List. (no_repeats(x,y:A//(x R y);L) ∧ (∀x:x,y:A//(x R y). (x ∈ L)))

---

Latex:

---

Latex:

1.  A  :  Type
2.  R  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  L  :  A  List
4.  no\_repeats(A;L)
5.  \mforall{}x:A.  (x  \mmember{}  L)
6.  EquivRel(A;x,y.x  R  y)
7.  \mforall{}x,y:A.    Dec(x  R  y)
\mvdash{}  \mexists{}L:(x,y:A//(x  R  y))  List.  (no\_repeats(x,y:A//(x  R  y);L)  \mwedge{}  (\mforall{}x:x,y:A//(x  R  y).  (x  \mmember{}  L)))


By

---

Latex:
(InstLemma  `decidable\_\_quotient\_equal`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index