---

Step * of Lemma alg_car_wf

∀A:Type. ∀a:algebra_sig{i:l}(A).  (a.car ∈ Type)
BY
{ ModulePiTac 10 ``alg_car`` }

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}a:algebra\_sig\{i:l\}(A).    (a.car  \mmember{}  Type)


By

---

Latex:
ModulePiTac  10  ``alg\_car``

---

Home Index