---

Step * of Lemma ctt-kind-0

No Annotations
∀[t:CttTerm]
  ∀X:?CubicalContext. [[X;t]] ⊆r Provisional''''(cttTerm(context-set(X))) supposing context-ok(X) 
  supposing ctt-kind(t) = 0 ∈ ℤ
BY
{ (InstLemma `assert-ctt-is-term` [] THEN RepeatFor 2 (ParallelLast')) }

1
.....antecedent..... 
1. t : CttTerm
2. ctt-kind(t) = 0 ∈ ℤ
⊢ ↑ctt-is-term(t)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[t:CttTerm]
    \mforall{}X:?CubicalContext.  [[X;t]]  \msubseteq{}r  Provisional''''(cttTerm(context-set(X)))  supposing  context-ok(X) 
    supposing  ctt-kind(t)  =  0


By

---

Latex:
(InstLemma  `assert-ctt-is-term`  []  THEN  RepeatFor  2  (ParallelLast'))

---

Home Index