---

Step * 2 1 of Lemma subtype_per-quotient

.....subterm..... T:t
2:n
1. T : Type
2. E : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.E[x;y])
4. a : Base
5. b : Base
6. c : a = b ∈ T
⊢ a = b ∈ (x,y:T/per/E[x;y])
BY
{ (At ⌜Type⌝ PerEqCD⋅ THEN Reduce 0 THEN Try (Fold `per-quotient` 0) THEN Auto)⋅ }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  T  :  Type
2.  E  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(T;x,y.E[x;y])
4.  a  :  Base
5.  b  :  Base
6.  c  :  a  =  b
\mvdash{}  a  =  b


By

---

Latex:
(At  \mkleeneopen{}Type\mkleeneclose{}  PerEqCD\mcdot{}  THEN  Reduce  0  THEN  Try  (Fold  `per-quotient`  0)  THEN  Auto)\mcdot{}

---

Home Index