---

Step * of Lemma image-type_wf

∀[A:Type]. ∀[f:Base].  (Image(A,f) ∈ Type)
BY
{ (TACTIC:Auto THEN TACTIC:(Unfold `member` 0 THEN Refine_imageEquality Type⋅ THEN Auto)) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:Base].    (Image(A,f)  \mmember{}  Type)


By

---

Latex:
(TACTIC:Auto  THEN  TACTIC:(Unfold  `member`  0  THEN  Refine\_imageEquality  Type\mcdot{}  THEN  Auto))

---

Home Index