---

Step * 1 1 1 1 1 2 1 1 of Lemma urec-level-property


1. F : Type ⟶ Type
2. con : Constr(T.F[T])
⊢ con [] ∈ F Void
BY
{ ((Assert [] ∈ Void List BY Auto) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  con  :  Constr(T.F[T])
\mvdash{}  con  []  \mmember{}  F  Void


By

---

Latex:
((Assert  []  \mmember{}  Void  List  BY  Auto)  THEN  Auto)\mcdot{}

---

Home Index