---

Step * 1 1 1 1 2 1 1 1 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)
8. d : ∀u,v:x,y:A//R[x;y].  Dec(u = v ∈ (x,y:A//R[x;y]))
9. x : Base
10. x1 : Base
11. x = x1 ∈ pertype(λx,y. ((x ∈ A) ∧ (y ∈ A) ∧ (x R y)))
12. x ∈ A
13. x1 ∈ A
14. x R x1
⊢ Ax ∈ ↓(x ∈ remove-repeats(mk_deq(d);L))
BY
{ (MemTypeCD THEN (GenConcl ⌜x = a ∈ A⌝⋅ 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. d : ∀u,v:x,y:A//R[x;y].  Dec(u = v ∈ (x,y:A//R[x;y]))
9. x : Base
10. x1 : Base
11. x = x1 ∈ pertype(λx,y. ((x ∈ A) ∧ (y ∈ A) ∧ (x R y)))
12. x ∈ A
13. x1 ∈ A
14. x R x1
15. a : A
16. x = a ∈ A
⊢ (a ∈ remove-repeats(mk_deq(d);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)
8.  d  :  \mforall{}u,v:x,y:A//R[x;y].    Dec(u  =  v)
9.  x  :  Base
10.  x1  :  Base
11.  x  =  x1
12.  x  \mmember{}  A
13.  x1  \mmember{}  A
14.  x  R  x1
\mvdash{}  Ax  \mmember{}  \mdownarrow{}(x  \mmember{}  remove-repeats(mk\_deq(d);L))


By

---

Latex:
(MemTypeCD  THEN  (GenConcl  \mkleeneopen{}x  =  a\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index