---

Step * of Lemma ctt-binder-context_wf

No Annotations
ctt-binder-context ∈ ?CubicalContext
⟶ (varname() List)
⟶ CttOp
⟶ very-dep-fun(?CubicalContext;varname() List × CttTerm;a,bt.[[a;snd(bt)]])
BY
{ (Unfold `ctt-binder-context` 0
   THEN RepeatFor 3 ((FunExt THENL [Id; Auto]))
   THEN Reduce 0
   THEN ((VeryDepFunCD''''' THENW Auto)
         THENL [(Reduce 0 THEN Auto THEN MemTypeCD THEN Reduce 0 THEN Auto)
               ; ((Reduce -1 THEN Reduce 0)
                  THEN (MemCD THENA Auto)
                  THEN ((BoolCase ⌜||L|| <z ||ctt-arity(x2)||⌝⋅ THENA Auto) THEN Try (Declaration))
                  THEN (BoolCase ⌜(||fst(bt)|| =z fst(ctt-arity(x2)[||L||]))⌝⋅ THENA Auto)
                  THEN Try (Declaration)
                  THEN (BoolCase ⌜bdd-all(||L||;i.(ctt-kind(snd(fst(snd(L[i])))) =z snd(ctt-arity(x2)[i])))⌝⋅
                        THENA Auto
                        )
                  THEN Try (Declaration)
                  THEN MemCD
                  THEN Try (Declaration)
                  THEN ((D -4 THEN Reduce 0 THEN Declaration) ORELSE ((MemTypeCD THENW Auto) THEN Try (Declaration))))]
   )
   THEN (Assert bind-provision(x;ctxt.OK(ctxt)) = x ∈ ?CubicalContext BY
               Auto)
   THEN BetterSplitAndConcl
   THEN Try (Hypothesis)
   THEN Try ((Intros THEN (RWO "6" 0 THENA Auto)))
   THEN (((RWO "first0" 0 THENA Auto) THEN Reduce 0 THEN (BoolCase ⌜0 <z ||ctt-arity(x2)||⌝⋅ THENA Auto))
         ORELSE ((RWO "length_firstn" 0 THENA Auto) THEN (BoolCase ⌜1 <z ||ctt-arity(x2)||⌝⋅ THENA Auto))
         ORELSE ((RWO "assert-bdd-all" (-4) THENA Auto) THEN ParallelOp -4 THEN RW assert_pushdownC (-1) THEN Auto))
   THEN ((RepUR ``bdd-all`` 0 THEN (RWW "band_tt" 0 THENA Auto)) THEN (RWW "select-firstn" 0 THENA Auto))
   THEN (SplitOnConclITE THENA Auto)
   THEN Try (Trivial)
   THEN RepUR ``provisional-subterm-context`` 0
   THEN (RWW "band_ff" 0 THENA Auto)
   THEN Reduce 0
   THEN RepUR ``ctt-subterm-context`` 0
   THEN RepeatFor 2 (((RWW "band_ff band_tt length_firstn" 0 THENA Auto) THEN Reduce 0))
   THEN SplitOrHyps
   THEN OnSomeHyp (\h. ((FLemma `ctt-opr-is-implies` [h] THENA Auto)
                        THEN HypSubst' (-1) 0
                        THEN RepUR ``ctt-opr-is`` 0
                        THEN Auto))⋅) }

---

Latex:

---

Latex:
No  Annotations
ctt-binder-context  \mmember{}  ?CubicalContext
{}\mrightarrow{}  (varname()  List)
{}\mrightarrow{}  CttOp
{}\mrightarrow{}  very-dep-fun(?CubicalContext;varname()  List  \mtimes{}  CttTerm;a,bt.[[a;snd(bt)]])


By

---

Latex:
(Unfold  `ctt-binder-context`  0
  THEN  RepeatFor  3  ((FunExt  THENL  [Id;  Auto]))
  THEN  Reduce  0
  THEN  ((VeryDepFunCD'''''  THENW  Auto)
              THENL  [(Reduce  0  THEN  Auto  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)
                          ;  ((Reduce  -1  THEN  Reduce  0)
                                THEN  (MemCD  THENA  Auto)
                                THEN  ((BoolCase  \mkleeneopen{}||L||  <z  ||ctt-arity(x2)||\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Try  (Declaration))
                                THEN  (BoolCase  \mkleeneopen{}(||fst(bt)||  =\msubz{}  fst(ctt-arity(x2)[||L||]))\mkleeneclose{}\mcdot{}  THENA  Auto)
                                THEN  Try  (Declaration)
                                THEN  (BoolCase 
                                            \mkleeneopen{}bdd-all(||L||;i.(ctt-kind(snd(fst(snd(L[i]))))  =\msubz{}  snd(ctt-arity(x2)[i])))\mkleeneclose{}\mcdot{}
                                            THENA  Auto
                                            )
                                THEN  Try  (Declaration)
                                THEN  MemCD
                                THEN  Try  (Declaration)
                                THEN  ((D  -4  THEN  Reduce  0  THEN  Declaration)
                                ORELSE  ((MemTypeCD  THENW  Auto)  THEN  Try  (Declaration))
                                ))]
  )
  THEN  (Assert  bind-provision(x;ctxt.OK(ctxt))  =  x  BY
                          Auto)
  THEN  BetterSplitAndConcl
  THEN  Try  (Hypothesis)
  THEN  Try  ((Intros  THEN  (RWO  "6"  0  THENA  Auto)))
  THEN  (((RWO  "first0"  0  THENA  Auto)
                THEN  Reduce  0
                THEN  (BoolCase  \mkleeneopen{}0  <z  ||ctt-arity(x2)||\mkleeneclose{}\mcdot{}  THENA  Auto))
              ORELSE  ((RWO  "length\_firstn"  0  THENA  Auto)
                              THEN  (BoolCase  \mkleeneopen{}1  <z  ||ctt-arity(x2)||\mkleeneclose{}\mcdot{}  THENA  Auto)
                              )
              ORELSE  ((RWO  "assert-bdd-all"  (-4)  THENA  Auto)
                              THEN  ParallelOp  -4
                              THEN  RW  assert\_pushdownC  (-1)
                              THEN  Auto))
  THEN  ((RepUR  ``bdd-all``  0  THEN  (RWW  "band\_tt"  0  THENA  Auto))
              THEN  (RWW  "select-firstn"  0  THENA  Auto)
              )
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  (Trivial)
  THEN  RepUR  ``provisional-subterm-context``  0
  THEN  (RWW  "band\_ff"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RepUR  ``ctt-subterm-context``  0
  THEN  RepeatFor  2  (((RWW  "band\_ff  band\_tt  length\_firstn"  0  THENA  Auto)  THEN  Reduce  0))
  THEN  SplitOrHyps
  THEN  OnSomeHyp  (\mbackslash{}h.  ((FLemma  `ctt-opr-is-implies`  [h]  THENA  Auto)
                                            THEN  HypSubst'  (-1)  0
                                            THEN  RepUR  ``ctt-opr-is``  0
                                            THEN  Auto))\mcdot{})

---

Home Index