---

Step * 1 of Lemma ctt-kind-1

.....antecedent..... 
1. t : CttTerm
2. ctt-kind(t) = 1 ∈ ℤ
⊢ ↑ctt-is-fibrant(t)
BY
{ (MoveToConcl (-1)
   THEN RepUR ``ctt-is-fibrant ctt-kind`` 0
   THEN InstLemma `isvarterm_wf` [⌜parm{i'}⌝]⋅
   THEN (BoolCase ⌜isvarterm(t)⌝⋅ THENA Auto)
   THEN ((GenConclTerm ⌜ctt-op-sort(term-opr(t))⌝⋅ THENA Complete (Auto)) ORELSE Auto)) }

1
1. t : CttTerm
2. ¬↑isvarterm(t)
3. ∀[opr:𝕌']. ∀[t:term(opr)].  (isvarterm(t) ∈ 𝔹)
4. v : {x:Atom| (x ∈ ``fibrant type term``)} 
5. ctt-op-sort(term-opr(t)) = v ∈ {x:Atom| (x ∈ ``fibrant type term``)} 
⊢ (if v =a "fibrant" then 1 if v =a "type" then 2 else 0 fi  = 1 ∈ ℤ) ⇒ (↑v =a "fibrant")

---

Latex:

---

Latex:
.....antecedent..... 
1.  t  :  CttTerm
2.  ctt-kind(t)  =  1
\mvdash{}  \muparrow{}ctt-is-fibrant(t)


By

---

Latex:
(MoveToConcl  (-1)
  THEN  RepUR  ``ctt-is-fibrant  ctt-kind``  0
  THEN  InstLemma  `isvarterm\_wf`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}
  THEN  (BoolCase  \mkleeneopen{}isvarterm(t)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ((GenConclTerm  \mkleeneopen{}ctt-op-sort(term-opr(t))\mkleeneclose{}\mcdot{}  THENA  Complete  (Auto))  ORELSE  Auto))

---

Home Index