---

Step * of Lemma mk_perm_wf_a

∀T:Type. ∀f,b:T ⟶ T.  (InvFuns(T;T;f;b) ⇒ (mk_perm(f;b) ∈ Perm(T)))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}f,b:T  {}\mrightarrow{}  T.    (InvFuns(T;T;f;b)  {}\mRightarrow{}  (mk\_perm(f;b)  \mmember{}  Perm(T)))


By

---

Latex:
Auto

---

Home Index