---

Step * 1 of Lemma truncate-map_wf


1. X : Type
2. Q : Type
3. f : X ⟶ ⇃(Q)
4. x : X
5. x1 : X
6. True
⊢ (|f| x) = (|f| x1) ∈ ⇃(Q)
BY
{ (BLemma `half-squash-equality` THEN RepUR ``truncate-map`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  Q  :  Type
3.  f  :  X  {}\mrightarrow{}  \00D9(Q)
4.  x  :  X
5.  x1  :  X
6.  True
\mvdash{}  (|f|  x)  =  (|f|  x1)


By

---

Latex:
(BLemma  `half-squash-equality`  THEN  RepUR  ``truncate-map``  0  THEN  Auto)

---

Home Index