---

Step * of Lemma ctt-meaning-type_wf

No Annotations
∀[X:⊢''']. ∀[t:CttTerm].  (ctt-meaning-type{i:l}(X;t) ∈ 𝕌{i'''''})
BY
{ (Intros
   THEN Unhide
   THEN RepUR ``ctt-meaning-type`` 0
   THEN (InstLemma `isvarterm_wf` [⌜parm{i'}⌝;⌜CttOp⌝;⌜t⌝]⋅ THENA Auto)
   THEN ((SplitOnConclITE THENA Auto)
         THENL [Auto
               ; ((InstLemma `term-opr_wf` [⌜parm{i'}⌝;⌜CttOp⌝;⌜t⌝]⋅ THENA Auto)
                  THEN Repeat ((SplitOnConclITE THENA Auto))
                  THEN Auto)]
   )) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:\mvdash{}'''].  \mforall{}[t:CttTerm].    (ctt-meaning-type\{i:l\}(X;t)  \mmember{}  \mBbbU{}\{i'''''\})


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  RepUR  ``ctt-meaning-type``  0
  THEN  (InstLemma  `isvarterm\_wf`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}CttOp\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((SplitOnConclITE  THENA  Auto)
              THENL  [Auto
                          ;  ((InstLemma  `term-opr\_wf`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}CttOp\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                THEN  Repeat  ((SplitOnConclITE  THENA  Auto))
                                THEN  Auto)]
  ))

---

Home Index