---

Step * of Lemma null_remove_leading

∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].  uiff(↑null(remove_leading(x.P[x];L));(∀x∈L.↑P[x]))
BY
{ xxx(InstLemma `remove_leading_property` []
      THEN RepeatFor 3 (ParallelLast')
      THEN ExRepD
      THEN MoveToConcl (-1)
      THEN (GenConclAtAddr [2;1;1;1]⋅ THENA (Auto THEN D -2 THEN All Reduce THEN Auto'))
      THEN (RepeatFor 2 (DVar `v')⋅
            THEN Reduce 0
            THEN Auto
            THEN (RWW  "append-nil" (-2) THENA Auto)
            THEN Try ((HypSubst (-2) 0 THEN Auto THEN BLemma `l_all_iff` THEN Auto)))
      THEN (HypSubst (-2) (-1) THENA Auto)
      THEN (RWO "l_all_append" (-1) THEN Auto)
      THEN RWO "l_all_cons" (-1)
      THEN Auto
      THEN All Reduce
      THEN OnMaybeHyp 7 (\h. (D h THEN Complete (Auto))))xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].    uiff(\muparrow{}null(remove\_leading(x.P[x];L));(\mforall{}x\mmember{}L.\muparrow{}P[x]))


By

---

Latex:
xxx(InstLemma  `remove\_leading\_property`  []
        THEN  RepeatFor  3  (ParallelLast')
        THEN  ExRepD
        THEN  MoveToConcl  (-1)
        THEN  (GenConclAtAddr  [2;1;1;1]\mcdot{}  THENA  (Auto  THEN  D  -2  THEN  All  Reduce  THEN  Auto'))
        THEN  (RepeatFor  2  (DVar  `v')\mcdot{}
                    THEN  Reduce  0
                    THEN  Auto
                    THEN  (RWW    "append-nil"  (-2)  THENA  Auto)
                    THEN  Try  ((HypSubst  (-2)  0  THEN  Auto  THEN  BLemma  `l\_all\_iff`  THEN  Auto)))
        THEN  (HypSubst  (-2)  (-1)  THENA  Auto)
        THEN  (RWO  "l\_all\_append"  (-1)  THEN  Auto)
        THEN  RWO  "l\_all\_cons"  (-1)
        THEN  Auto
        THEN  All  Reduce
        THEN  OnMaybeHyp  7  (\mbackslash{}h.  (D  h  THEN  Complete  (Auto))))xxx

---

Home Index