---

Step * of Lemma ap-con_wf

∀[F:Type ⟶ Type]. ∀[T:{T:Type| T ⊆r Base} ]. ∀[con:Constr(T.F[T])]. ∀[L:T List].  (ap-con(con;L) ∈ F[T])
BY
{ (BasicUniformUnivCD Auto THEN Unfolds ``member ap-con`` 0 THEN With ⌜T⌝ (DVar `con')⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  \mforall{}[T:\{T:Type|  T  \msubseteq{}r  Base\}  ].  \mforall{}[con:Constr(T.F[T])].  \mforall{}[L:T  List].
    (ap-con(con;L)  \mmember{}  F[T])


By

---

Latex:
(BasicUniformUnivCD  Auto  THEN  Unfolds  ``member  ap-con``  0  THEN  With  \mkleeneopen{}T\mkleeneclose{}  (DVar  `con')\mcdot{}  THEN  Auto)

---

Home Index