---

Step * of Lemma perm_b_wf

∀T:Type. ∀p:perm_sig(T).  (p.b ∈ T ⟶ T)
BY
{ ModulePiTac 2 ``perm_f perm_b`` }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}p:perm\_sig(T).    (p.b  \mmember{}  T  {}\mrightarrow{}  T)


By

---

Latex:
ModulePiTac  2  ``perm\_f  perm\_b``

---

Home Index