---

Step * 1 of Lemma imagetype_wf


1. A : Type
2. f : Base
3. Trans(Base;x,y.image-per(A;f) x y)
4. x : Base
5. y : Base
6. image-per(A;f) x y
⊢ image-per(A;f) y x
BY
{ (InstLemma `image-per-symmetric` [⌜A⌝;⌜f⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  Base
3.  Trans(Base;x,y.image-per(A;f)  x  y)
4.  x  :  Base
5.  y  :  Base
6.  image-per(A;f)  x  y
\mvdash{}  image-per(A;f)  y  x


By

---

Latex:
(InstLemma  `image-per-symmetric`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index