---

Step * 1 1 1 of Lemma ctt-kind-0


1. t : CttTerm
2. ¬↑isvarterm(t)
3. ∀[opr:𝕌']. ∀[t:term(opr)].  (isvarterm(t) ∈ 𝔹)
4. v : Atom
5. [%13] : (v ∈ ``fibrant type term``)
6. ctt-op-sort(term-opr(t)) = v ∈ {x:Atom| (x ∈ ``fibrant type term``)} 
7. (v ∈ ``fibrant type term``)
⊢ (if v =a "fibrant" then 1 if v =a "type" then 2 else 0 fi  = 0 ∈ ℤ) ⇒ (↑v =a "term")
BY
{ (RepeatFor 2 ((GenListD (-1) THEN (D -1 THENL [(HypSubst' (-1) 0 THEN Reduce 0 THEN Auto); Id])))
   THEN GenListD (-1)
   THEN HypSubst' (-1) 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  t  :  CttTerm
2.  \mneg{}\muparrow{}isvarterm(t)
3.  \mforall{}[opr:\mBbbU{}'].  \mforall{}[t:term(opr)].    (isvarterm(t)  \mmember{}  \mBbbB{})
4.  v  :  Atom
5.  [\%13]  :  (v  \mmember{}  ``fibrant  type  term``)
6.  ctt-op-sort(term-opr(t))  =  v
7.  (v  \mmember{}  ``fibrant  type  term``)
\mvdash{}  (if  v  =a  "fibrant"  then  1  if  v  =a  "type"  then  2  else  0  fi    =  0)  {}\mRightarrow{}  (\muparrow{}v  =a  "term")


By

---

Latex:
(RepeatFor  2  ((GenListD  (-1)  THEN  (D  -1  THENL  [(HypSubst'  (-1)  0  THEN  Reduce  0  THEN  Auto);  Id])))
  THEN  GenListD  (-1)
  THEN  HypSubst'  (-1)  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index