---

Step * of Lemma truncate-map_wf

∀[X,Q:Type].  ∀f:X ⟶ ⇃(Q). (|f| ∈ ⇃(X) ⟶ ⇃(Q))
BY
{ (Auto THEN (FunExt THENW Auto) THEN quotD (-1)) }

1
1. X : Type
2. Q : Type
3. f : X ⟶ ⇃(Q)
4. x : X
5. x1 : X
6. True
⊢ (|f| x) = (|f| x1) ∈ ⇃(Q)

---

Latex:

---

Latex:
\mforall{}[X,Q:Type].    \mforall{}f:X  {}\mrightarrow{}  \00D9(Q).  (|f|  \mmember{}  \00D9(X)  {}\mrightarrow{}  \00D9(Q))


By

---

Latex:
(Auto  THEN  (FunExt  THENW  Auto)  THEN  quotD  (-1))

---

Home Index