Theory llist

⊢ (∀x. [||] ++ₗ x = x) ∧ ∀h t x. h:::t ++ₗ x = h:::(t ++ₗ x)

⊢ ∀h t.
    h:::t = llist_abs (λn. if n = 0 then SOME h else llist_rep t (n − 1))

⊢ (∀ll. LDROP 0 ll = SOME ll) ∧
  ∀n ll. LDROP (SUC n) ll = OPTION_JOIN (OPTION_MAP (LDROP n) (LTL ll))

⊢ (∀P. LDROP_WHILE P [||] = [||]) ∧
  (∀P x xs.
     LDROP_WHILE P (x:::xs) = if P x then LDROP_WHILE P xs else x:::xs) ∧
  ∀P l. every P l ⇒ LDROP_WHILE P l = [||]

⊢ ∀P ll.
    LFILTER P ll =
    if ¬exists P ll then [||]
    else if P (THE (LHD ll)) then THE (LHD ll):::LFILTER P (THE (LTL ll))
    else LFILTER P (THE (LTL ll))

⊢ ∀ll.
    LFLATTEN ll =
    if every ($= [||]) ll then [||]
    else if THE (LHD ll) = [||] then LFLATTEN (THE (LTL ll))
    else
      THE (LHD (THE (LHD ll))):::
          LFLATTEN (THE (LTL (THE (LHD ll))):::THE (LTL ll))

⊢ (∀f. LGENLIST f NONE = LUNFOLD (λn. SOME (n + 1,f n)) 0) ∧
  ∀f lim.
    LGENLIST f (SOME lim) =
    LUNFOLD (λn. if n < lim then SOME (n + 1,f n) else NONE) 0

⊢ ∀ll. LHD ll = llist_rep ll 0

⊢ ∀ll.
    LLENGTH ll = if LFINITE ll then SOME (@n. llength_rel ll n) else NONE

⊢ (∀f. LMAP f [||] = [||]) ∧ ∀f h t. LMAP f (h:::t) = f h:::LMAP f t

⊢ [||] = llist_abs (λn. NONE)

⊢ (∀ll. LNTH 0 ll = LHD ll) ∧
  ∀n ll. LNTH (SUC n) ll = OPTION_JOIN (OPTION_MAP (LNTH n) (LTL ll))

⊢ ∀l1 l2.
    LPREFIX l1 l2 ⇔
    case toList l1 of
      NONE => l1 = l2
    | SOME xs =>
      case toList l2 of
        NONE => LTAKE (LENGTH xs) l2 = SOME xs
      | SOME ys => xs ≼ ys

⊢ ∀l. LREPEAT l =
      if NULL l then [||] else LGENLIST (λn. l❲n MOD LENGTH l❳) NONE

⊢ ∀l x. LSET l x ⇔ ∃n. LNTH n l = SOME x

⊢ ∀xs zs. LSUFFIX xs zs ⇔ ∃ys. xs = fromList ys ++ₗ zs ∨ zs = [||]

⊢ (∀ll. LTAKE 0 ll = SOME []) ∧
  ∀n ll.
    LTAKE (SUC n) ll =
    case LHD ll of
      NONE => NONE
    | SOME hd =>
      case LTAKE n (THE (LTL ll)) of
        NONE => NONE
      | SOME tl => SOME (hd::tl)

⊢ (∀P. LTAKE_WHILE P [||] = [||]) ∧
  (∀P x xs.
     LTAKE_WHILE P (x:::xs) = if P x then x:::LTAKE_WHILE P xs else [||]) ∧
  ∀P l. every P l ⇒ LTAKE_WHILE P l = l

⊢ ∀ll.
    LTL ll =
    case LHD ll of
      NONE => NONE
    | SOME v => SOME (llist_abs (λn. llist_rep ll (n + 1)))

⊢ ∀ll.
    LTL_HD ll =
    case llist_rep ll 0 of
      NONE => NONE
    | SOME h => SOME (llist_abs (llist_rep ll ∘ SUC),h)

⊢ ∀f z.
    LUNFOLD f z =
    llist_abs
      (λn.
           OPTION_MAP SND
             (FUNPOW (λm. OPTION_BIND m (UNCURRY (K ∘ f))) n (f z)))

⊢ LUNZIP [||] = ([||],[||]) ∧
  ∀x y t.
    LUNZIP ((x,y):::t) = (let (ll1,ll2) = LUNZIP t in (x:::ll1,y:::ll2))

⊢ (∀l1. LZIP (l1,[||]) = [||]) ∧ (∀l2. LZIP ([||],l2) = [||]) ∧
  ∀h1 h2 t1 t2. LZIP (h1:::t1,h2:::t2) = (h1,h2):::LZIP (t1,t2)

⊢ ∀P ll. every P ll ⇔ ¬exists ($¬ ∘ P) ll

⊢ fromList [] = [||] ∧ ∀h t. fromList (h::t) = h:::fromList t

⊢ ∀f. fromSeq f = LUNFOLD (λx. SOME (SUC x,f x)) 0

⊢ ∀ll f. lbind ll f = LFLATTEN (LMAP f ll)

⊢ ∀lo.
    linear_order_to_list_f lo =
    (let
       min = minimal_elements (domain lo ∪ range lo) lo
     in
       if min = ∅ then NONE
       else SOME (rrestrict lo (domain lo ∪ range lo DIFF min),CHOICE min))

⊢ ∀ll b f.
    llist_CASE ll b f =
    case LTL_HD ll of NONE => b | SOME (ltl,lhd) => f lhd ltl

⊢ ∃rep. TYPE_DEFINITION lrep_ok rep

⊢ (∀a. llist_abs (llist_rep a) = a) ∧
  ∀r. lrep_ok r ⇔ llist_rep (llist_abs r) = r

⊢ ∀R l1 l2.
    llist_rel R l1 l2 ⇔
    LLENGTH l1 = LLENGTH l2 ∧
    ∀i x y. LNTH i l1 = SOME x ∧ LNTH i l2 = SOME y ⇒ R x y

⊢ ∀ll. toList ll = if LFINITE ll then LTAKE (THE (LLENGTH ll)) ll else NONE

⊢ GENLIST f n = h::t ⇔ 0 < n ∧ f 0 = h ∧ t = GENLIST (f ∘ SUC) (n − 1)

⊢ ∀x l. x ∈ LSET l ⇔ ∃n. LNTH n l = SOME x

⊢ ∀l1 l2 l3. LFINITE l1 ⇒ (l1 ++ₗ l2 = l1 ++ₗ l3 ⇔ l2 = l3)

⊢ ∀ll1 ll2 ll3. ll1 ++ₗ ll2 ++ₗ ll3 = ll1 ++ₗ (ll2 ++ₗ ll3)

⊢ l1 ++ₗ l2 = [||] ⇔ l1 = [||] ∧ l2 = [||]

⊢ ∀ll. ll ++ₗ [||] = ll

⊢ ∀l1 l2. fromList l1 ++ₗ fromList l2 = fromList (l1 ⧺ l2)

⊢ (∀f ll. fromSeq f ++ₗ ll = fromSeq f) ∧
  ∀l f.
    fromList l ++ₗ fromSeq f =
    fromSeq (λn. if n < LENGTH l then l❲n❳ else f (n − LENGTH l))

⊢ ∀h1 t1 h2 t2. h1:::t1 = h2:::t2 ⇔ h1 = h2 ∧ t1 = t2

⊢ ∀h t. h:::t ≠ [||] ∧ [||] ≠ h:::t

⊢ LDROP 1 = LTL

⊢ LDROP 1 (h:::t) = SOME t

⊢ ∀k1 k2 x.
    LDROP (k1 + k2) x =
    case LDROP k1 x of NONE => NONE | SOME ll => LDROP k2 ll

⊢ LDROP n l1 = SOME l ⇒ LDROP n (l1 ++ₗ l2) = SOME (l ++ₗ l2)

⊢ LDROP n ll = SOME [||] ⇔ LLENGTH ll = SOME n

⊢ ∀n ll. LDROP n ll = FUNPOW (λm. OPTION_BIND m LTL) n (SOME ll)

⊢ ∀n xs a t. LDROP n xs = SOME (a:::t) ⇒ LNTH n xs = SOME a

⊢ ∀ll k1 k2.
    ¬LFINITE ll ⇒
    THE (LDROP k2 (THE (LDROP k1 ll))) = THE (LDROP k1 (THE (LDROP k2 ll)))

⊢ LDROP k l = NONE ⇒ LFINITE l

⊢ LDROP n ll = SOME l ∧ LLENGTH ll = SOME m ⇒
  n ≤ m ∧ LLENGTH l = SOME (m − n)

⊢ LDROP (SUC n) ls = OPTION_BIND (LDROP n ls) LTL

⊢ (∀ll. LDROP 0 ll = SOME ll) ∧ (∀n. LDROP (SUC n) [||] = NONE) ∧
  ∀n h t. LDROP (SUC n) (h:::t) = LDROP n t

⊢ ∀ls n.
    LDROP n (fromList ls) =
    if n ≤ LENGTH ls then SOME (fromList (DROP n ls)) else NONE

⊢ ∀n f. LDROP n (fromSeq f) = SOME (fromSeq (f ∘ $+ n))

⊢ ∀P ll1 ll2.
    LFINITE ll1 ⇒ LFILTER P (ll1 ++ₗ ll2) = LFILTER P ll1 ++ₗ LFILTER P ll2

⊢ LFILTER P ll = h:::t ⇒
  ∃l ll'.
    ll = fromList l ++ₗ h:::ll' ∧ EVERY ($¬ ∘ P) l ∧ P h ∧
    LFILTER P ll' = t

⊢ ∀ll. LFILTER P ll = [||] ⇔ every ($¬ ∘ P) ll

⊢ ∀P ll. every ($¬ ∘ P) ll ⇒ LFILTER P ll = [||]

⊢ (∀P. LFILTER P [||] = [||]) ∧
  ∀P h t. LFILTER P (h:::t) = if P h then h:::LFILTER P t else LFILTER P t

⊢ ∀p l. LFILTER p (fromList l) = fromList (FILTER p l)

⊢ ∀p f.
    LFILTER p (fromSeq f) =
    if ∀i. ¬p (f i) then [||]
    else if p (f 0) then f 0:::LFILTER p (fromSeq (f ∘ SUC))
    else LFILTER p (fromSeq (f ∘ SUC))

⊢ LFINITE ll ⇔ ∃n. LTAKE n ll = NONE

⊢ ∀ll1 ll2. LFINITE (ll1 ++ₗ ll2) ⇔ LFINITE ll1 ∧ LFINITE ll2

⊢ ∀n ll. LFINITE ll ∧ n ≤ THE (LLENGTH ll) ⇒ ∃y. LDROP n ll = SOME y

⊢ ∀ll. LFINITE ll ⇒ ∃n. LLENGTH ll = SOME n

⊢ ∀ll. LFINITE ll ⇒ ∃l. ll = fromList l

⊢ ∀P. P [||] ∧ (∀h t. P t ⇒ P (h:::t)) ⇒ ∀a0. LFINITE a0 ⇒ P a0

⊢ ∀ll. LFINITE ll ⇒ ∀l2. ll ++ₗ l2 = ll ⇒ l2 = [||]

⊢ ∀ll. LFINITE ll ⇒ LFINITE (LFILTER P ll)

⊢ LFINITE (LFLATTEN ll) ⇔
  LFINITE (LFILTER ($¬ ∘ $= [||]) ll) ∧ every LFINITE ll

⊢ ∀lll.
    every (λll. LFINITE ll ∧ ll ≠ [||]) lll ⇒
    (LFINITE (LFLATTEN lll) ⇔ LFINITE lll)

⊢ LFINITE (LGENLIST f n) ⇔ n ≠ NONE

⊢ LFINITE ll ⇔ ∃n. LLENGTH ll = SOME n

⊢ ∀n ll. LFINITE ll ⇒ (IS_SOME (LNTH n ll) ⇔ n < THE (LLENGTH ll))

⊢ LFINITE ll ⇔ ∃n. LNTH n ll = NONE

⊢ ∀f ll. LFINITE (LMAP f ll) ⇔ LFINITE ll

⊢ P [||] ∧ (∀h t. LFINITE t ∧ P t ⇒ P (h:::t)) ⇒ ∀a0. LFINITE a0 ⇒ P a0

⊢ ∀n ll. LFINITE ll ∧ n ≤ THE (LLENGTH ll) ⇒ ∃y. LTAKE n ll = SOME y

⊢ (LFINITE [||] ⇔ T) ∧ ∀h t. LFINITE (h:::t) ⇔ LFINITE t

⊢ ∀a0. LFINITE a0 ⇔ a0 = [||] ∨ ∃h t. a0 = h:::t ∧ LFINITE t

⊢ ∀l. LFINITE (fromList l)

⊢ ∀f. ¬LFINITE (fromSeq f)

⊢ ∀LFINITE'.
    LFINITE' [||] ∧ (∀h t. LFINITE' t ⇒ LFINITE' (h:::t)) ⇒
    ∀a0. LFINITE a0 ⇒ LFINITE' a0

⊢ LFINITE [||] ∧ ∀h t. LFINITE t ⇒ LFINITE (h:::t)

⊢ ∀LFINITE'.
    LFINITE' [||] ∧ (∀h t. LFINITE t ∧ LFINITE' t ⇒ LFINITE' (h:::t)) ⇒
    ∀a0. LFINITE a0 ⇒ LFINITE' a0

⊢ ∀ll. LFINITE ll ⇒ ∃l. toList ll = SOME l

⊢ LFINITE ll ⇔ IS_SOME (toList ll)

⊢ ∀h t. LFLATTEN (h:::t) = h ++ₗ LFLATTEN t

⊢ ∀l1 l2. LFINITE l1 ⇒ LFLATTEN (l1 ++ₗ l2) = LFLATTEN l1 ++ₗ LFLATTEN l2

⊢ LFLATTEN ll = h:::t ⇔
  ∃p e t1 t2.
    ll = p ++ₗ (h:::t1):::t2 ∧ LFINITE p ∧ every ($= [||]) p ∧
    t = t1 ++ₗ LFLATTEN t2

⊢ ∀ll. LFLATTEN ll = [||] ⇔ every ($= [||]) ll

⊢ ∀h. LFLATTEN [|h|] = h

⊢ LFLATTEN [||] = [||] ∧ (∀tl. LFLATTEN ([||]:::t) = LFLATTEN t) ∧
  ∀h t tl. LFLATTEN ((h:::t):::tl) = h:::LFLATTEN (t:::tl)

⊢ ∀l. LFLATTEN (fromList (MAP fromList l)) = fromList (FLAT l)

⊢ EVERY ($= [||]) l ⇒ LFLATTEN (fromList l) = [||]

⊢ LGENLIST f NONE = fromList (GENLIST f n) ++ₗ LGENLIST (f ∘ $+ n) NONE

⊢ LGENLIST f NONE = h:::t ⇔ h = f 0 ∧ t = LGENLIST (f ∘ $+ 1) NONE

⊢ (LGENLIST f n = [||] ⇔ n = SOME 0) ∧ ([||] = LGENLIST f n ⇔ n = SOME 0)

⊢ ∀f k. LGENLIST f (SOME k) = fromList (GENLIST f k)

⊢ ∀f. LGENLIST f NONE = fromSeq f

⊢ LGENLIST f (SOME 0) = [||] ∧
  ∀n. LGENLIST f (SOME (SUC n)) = f 0:::LGENLIST (f ∘ SUC) (SOME n)

⊢ LGENLIST f (SOME n) = h:::t ⇔
  0 < n ∧ f 0 = h ∧ t = LGENLIST (f ∘ SUC) (SOME (n − 1))

⊢ LGENLIST f (SOME 0) = [||] ∧
  (∀n. LGENLIST f (SOME (NUMERAL (BIT1 n))) =
       f 0:::LGENLIST (f ∘ SUC) (SOME (NUMERAL (BIT1 n) − 1))) ∧
  ∀n. LGENLIST f (SOME (NUMERAL (BIT2 n))) =
      f 0:::LGENLIST (f ∘ SUC) (SOME (NUMERAL (BIT1 n)))

⊢ ∀h t. LHD (h:::t) = SOME h ∧ LTL (h:::t) = SOME t

⊢ ∀h t ll. ll = h:::t ⇔ LHD ll = SOME h ∧ LTL ll = SOME t

⊢ ∀ll. (LHD ll = NONE ⇔ ll = [||]) ∧ (NONE = LHD ll ⇔ ll = [||])

⊢ LHD (l1 ++ₗ l2) = if l1 = [||] then LHD l2 else LHD l1

⊢ LHD (h:::t) = SOME h

⊢ LHD (LGENLIST f limopt) = if limopt = SOME 0 then NONE else SOME (f 0)

⊢ LHD (LREPEAT l) = LHD (fromList l)

⊢ LHD (LUNFOLD f x) = OPTION_MAP SND (f x)

⊢ LHD [||] = NONE ∧ ∀h t. LHD (h:::t) = SOME h

⊢ LHD (fromList l) = if NULL l then NONE else SOME (HD l)

⊢ ∀f. LHD (fromSeq f) = SOME (f 0)

⊢ LLENGTH x = SOME 0 ⇔ x = [||]

⊢ ∀ll1 ll2.
    LLENGTH (ll1 ++ₗ ll2) =
    if LFINITE ll1 ∧ LFINITE ll2 then
      SOME (THE (LLENGTH ll1) + THE (LLENGTH ll2))
    else NONE

⊢ ∀f. LLENGTH (LGENLIST f limopt) = limopt

⊢ LLENGTH (LREPEAT l) = if NULL l then SOME 0 else NONE

⊢ ∀ll f. LLENGTH (LMAP f ll) = LLENGTH ll

⊢ LLENGTH [||] = SOME 0 ∧
  ∀h t. LLENGTH (h:::t) = OPTION_MAP SUC (LLENGTH t)

⊢ ∀l. LLENGTH (fromList l) = SOME (LENGTH l)

⊢ ∀f. LLENGTH (fromSeq f) = NONE

⊢ ∀ll1 ll2.
    ll1 = ll2 ⇔
    ∃R. R ll1 ll2 ∧
        ∀ll3 ll4.
          R ll3 ll4 ⇒
          ll3 = [||] ∧ ll4 = [||] ∨
          LHD ll3 = LHD ll4 ∧ R (THE (LTL ll3)) (THE (LTL ll4))

⊢ ∀ll1 ll2.
    ll1 = ll2 ⇔
    ∃R. R ll1 ll2 ∧
        ∀ll3 ll4.
          R ll3 ll4 ⇒
          ll3 = [||] ∧ ll4 = [||] ∨
          ∃h t1 t2. ll3 = h:::t1 ∧ ll4 = h:::t2 ∧ R t1 t2

⊢ ∀ll2 ll1.
    (∃R. R ll1 ll2 ∧
         ∀ll3 ll4.
           R ll3 ll4 ⇒
           ll3 = [||] ∧ ll4 = [||] ∨
           LHD ll3 = LHD ll4 ∧ R (THE (LTL ll3)) (THE (LTL ll4))) ⇒
    ll1 = ll2

⊢ ∀ll1 ll2 R.
    R ll1 ll2 ∧
    (∀ll3 ll4.
       R ll3 ll4 ⇒
       ll3 = [||] ∧ ll4 = [||] ∨
       LHD ll3 = LHD ll4 ∧ llist_upto R (THE (LTL ll3)) (THE (LTL ll4))) ⇒
    ll1 = ll2

⊢ ∀M M' v f.
    M = M' ∧ (M' = [||] ⇒ v = v') ∧
    (∀a0 a1. M' = a0:::a1 ⇒ f a0 a1 = f' a0 a1) ⇒
    llist_CASE M v f = llist_CASE M' v' f'

⊢ ∀f'.
    f' (llist_CASE x v f) ⇔ x = [||] ∧ f' v ∨ ∃a l. x = a:::l ∧ f' (f a l)

⊢ llist_CASE x v f = v' ⇔ x = [||] ∧ v = v' ∨ ∃a l. x = a:::l ∧ f a l = v'

⊢ ∀a1 a0. [||] ≠ a0:::a1

⊢ ∀f g.
    (∀x. f x = [||] ∧ g x = [||] ∨ ∃h y. f x = h:::f y ∧ g x = h:::g y) ⇒
    ∀x. f x = g x

⊢ ∀ll1 ll2.
    ll1 = ll2 ⇔
    ∃R. R ll1 ll2 ∧
        ∀ll3 ll4.
          R ll3 ll4 ⇒
          ll3 = ll4 ∨ ∃h t1 t2. ll3 = h:::t1 ∧ ll4 = h:::t2 ∧ R t1 t2

⊢ (every P [||] ⇔ T) ∧ (every P (h:::t) ⇔ P h ∧ every P t)

⊢ ∀f ll1 ll2. LMAP f (ll1 ++ₗ ll2) = LMAP f ll1 ++ₗ LMAP f ll2

⊢ ∀ll ll1 ll2.
    LFINITE ll1 ⇒
    (LMAP f ll = ll1 ++ₗ ll2 ⇔
     ∃ll10 ll20. ll = ll10 ++ₗ ll20 ∧ LMAP f ll10 = ll1 ∧ LMAP f ll20 = ll2)

⊢ LMAP f l = h:::t ⇔ ∃h0 t0. l = h0:::t0 ∧ h = f h0 ∧ t = LMAP f t0

⊢ (LMAP f l = [||] ⇔ l = [||]) ∧ ([||] = LMAP f l ⇔ l = [||])

⊢ LMAP f (LGENLIST g limopt) = LGENLIST (f ∘ g) limopt

⊢ ∀f g s.
    LMAP f (LUNFOLD g s) =
    LUNFOLD (λs. OPTION_MAP (λ(x,y). (x,f y)) (g s)) s

⊢ ∀f g ll. LMAP f (LMAP g ll) = LMAP (f ∘ g) ll

⊢ LMAP f (fromList l) = fromList (MAP f l)

⊢ ∀f g. LMAP f (fromSeq g) = fromSeq (f ∘ g)

⊢ ∀a b ll. LNTH (a + b) ll = OPTION_BIND (LDROP a ll) (LNTH b)

⊢ ∀ll1 ll2. ll1 = ll2 ⇔ ∀n. LNTH n ll1 = LNTH n ll2

⊢ ∀n ll. LNTH n ll = OPTION_BIND (LDROP n ll) LHD

⊢ ∀n ll. IS_SOME (LNTH n ll) ⇔ LFINITE ll ⇒ n < THE (LLENGTH ll)

⊢ ∀m n l. IS_SOME (LNTH n l) ∧ m ≤ n ⇒ IS_SOME (LNTH m l)

⊢ LNTH n (l1 ++ₗ l2) =
  case LLENGTH l1 of
    NONE => LNTH n l1
  | SOME m => if n < m then LNTH n l1 else LNTH (n − m) l2

⊢ ∀n l x. LNTH n l = SOME x ⇒ LHD (THE (LDROP n l)) = SOME x

⊢ ∀n f lim.
    LNTH n (LGENLIST f lim) =
    case lim of
      NONE => SOME (f n)
    | SOME lim0 => if n < lim0 then SOME (f n) else NONE

⊢ ∀x n l. LLENGTH l = SOME x ∧ x ≤ n ⇒ LNTH n l = NONE

⊢ ∀n f l. LNTH n (LMAP f l) = OPTION_MAP f (LNTH n l)

⊢ LNTH 0 (LUNFOLD f x) = OPTION_MAP SND (f x) ∧
  LNTH (SUC n) (LUNFOLD f x) =
  case f x of NONE => NONE | SOME (tx,hx) => LNTH n (LUNFOLD f tx)

⊢ LNTH 0 (LUNFOLD f x) = OPTION_MAP SND (f x) ∧
  (∀n. LNTH (NUMERAL (BIT1 n)) (LUNFOLD f x) =
       case f x of
         NONE => NONE
       | SOME (tx,hx) => LNTH (NUMERAL (BIT1 n) − 1) (LUNFOLD f tx)) ∧
  ∀n. LNTH (NUMERAL (BIT2 n)) (LUNFOLD f x) =
      case f x of
        NONE => NONE
      | SOME (tx,hx) => LNTH (NUMERAL (BIT1 n)) (LUNFOLD f tx)

⊢ ∀m n l. LNTH m l = NONE ∧ m ≤ n ⇒ LNTH n l = NONE

⊢ (∀n. LNTH n [||] = NONE) ∧ (∀h t. LNTH 0 (h:::t) = SOME h) ∧
  ∀n h t. LNTH (SUC n) (h:::t) = LNTH n t

⊢ LNTH n (fromList l) = if n < LENGTH l then SOME l❲n❳ else NONE

⊢ ∀n f. LNTH n (fromSeq f) = SOME (f n)

⊢ ∀i ll. LNTH i ll = llist_rep ll i

⊢ LPREFIX l1 l2 ∧ LPREFIX l2 l1 ⇒ l1 = l2

⊢ LPREFIX l1 l2 ⇔ ∃ll. l2 = l1 ++ₗ ll

⊢ LPREFIX (fromList l ++ₗ l1) (fromList l ++ₗ l2) ⇔ LPREFIX l1 l2

⊢ (∀ll h t. LPREFIX ll (h:::t) ⇔ ll = [||] ∨ ∃l. ll = h:::l ∧ LPREFIX l t) ∧
  ∀h t ll. LPREFIX (h:::t) ll ⇔ ∃l. ll = h:::l ∧ LPREFIX t l

⊢ LPREFIX [||] ll ∧ (LPREFIX ll [||] ⇔ ll = [||])

⊢ LPREFIX ll (LUNFOLD f n) ⇔
  case f n of
    NONE => ll = [||]
  | SOME (n,x) => ∀h t. ll = h:::t ⇒ h = x ∧ LPREFIX t (LUNFOLD f n)

⊢ LPREFIX l1 l2 ⇔ ∀i v. LNTH i l1 = SOME v ⇒ LNTH i l2 = SOME v

⊢ LPREFIX ll ll

⊢ LPREFIX l1 l2 ∧ LPREFIX l2 l3 ⇒ LPREFIX l1 l3

⊢ ∀l ll.
    LPREFIX (fromList l) ll ⇔
    case toList ll of
      NONE => LTAKE (LENGTH l) ll = SOME l
    | SOME ys => l ≼ ys

⊢ (LREPEAT l = [||] ⇔ l = []) ∧ ([||] = LREPEAT l ⇔ l = [])

⊢ LREPEAT [] = [||]

⊢ LREPEAT l = fromList l ++ₗ LREPEAT l

⊢ LSET [||] = ∅ ∧ LSET (x:::xs) = x INSERT LSET xs

⊢ LSET (l1 ++ₗ l2) = LSET l1 ∪ if LFINITE l1 then LSET l2 else ∅

⊢ x ∈ LSET ll ⇔ ∃p s. ll = p ++ₗ x:::s ∧ LFINITE p

⊢ LSET (LFLATTEN ll) =
  {e |
   ∃p e0 s. ll = p ++ₗ e0:::s ∧ e ∈ LSET e0 ∧ LFINITE p ∧ every LFINITE p}

⊢ x ∈ LSET ll ⇔ exists ($= x) ll

⊢ LSET (fromList l) = set l

⊢ LSET (lbind ll f) =
  {e |
   ∃p e0 s.
     ll = p ++ₗ e0:::s ∧ LFINITE p ∧ every (LFINITE ∘ f) p ∧
     e ∈ LSET (f e0)}

⊢ (LSUFFIX l [||] ⇔ T) ∧ (LSUFFIX [||] (y:::ys) ⇔ F) ∧
  (LSUFFIX (x:::xs) l ⇔ x:::xs = l ∨ LSUFFIX xs l)

⊢ ∀x y. LSUFFIX x y ∧ LSUFFIX y x ∧ LFINITE x ⇒ x = y

⊢ ∀s. LSUFFIX s s

⊢ ∀x y z. LSUFFIX x y ∧ LSUFFIX y z ⇒ LSUFFIX x z

⊢ ∀xs ys. LSUFFIX (fromList xs) (fromList ys) ⇔ IS_SUFFIX xs ys

⊢ ∀m h t. LTAKE m (h:::t) = NONE ⇔ ∃n. m = SUC n ∧ LTAKE n t = NONE

⊢ ∀m h t l.
    LTAKE m (h:::t) = SOME l ⇔
    m = 0 ∧ l = [] ∨ ∃n l'. m = SUC n ∧ LTAKE n t = SOME l' ∧ l = h::l'

⊢ (∀n ll.
     ¬LFINITE ll ⇒ fromList (THE (LTAKE n ll)) ++ₗ THE (LDROP n ll) = ll) ∧
  ∀n ll.
    LFINITE ll ∧ n ≤ THE (LLENGTH ll) ⇒
    fromList (THE (LTAKE n ll)) ++ₗ THE (LDROP n ll) = ll

⊢ ∀ll1 ll2. ll1 = ll2 ⇔ ∀n. LTAKE n ll1 = LTAKE n ll2

⊢ ∀n ll. LTAKE n ll = NONE ⇒ LNTH n ll = NONE

⊢ ∀n l x. LTAKE n l = SOME x ⇒ ∀h. ∃y. LTAKE n (h:::l) = SOME y

⊢ ∀n ll l1.
    LTAKE n ll = SOME l1 ⇒
    ∃l2. LDROP n ll = SOME l2 ∧ fromList l1 ++ₗ l2 = ll

⊢ ∀n l1 l2. IS_SOME (LTAKE n l1) ⇒ LTAKE n (l1 ++ₗ l2) = LTAKE n l1

⊢ ∀n l1 l2.
    LTAKE n l1 = NONE ⇒
    LTAKE n (l1 ++ₗ l2) =
    OPTION_MAP ($++ (THE (toList l1))) (LTAKE (n − THE (LLENGTH l1)) l2)

⊢ ∀ll l n.
    LTAKE (n + LENGTH l) (fromList l ++ₗ ll) =
    OPTION_MAP ($++ l) (LTAKE n ll)

⊢ ∀n ll l. LTAKE n ll = SOME l ⇒ n = LENGTH l

⊢ LLENGTH ll = SOME n ∧ n < m ⇒ LTAKE m ll = NONE

⊢ LLENGTH ll = SOME n ⇒ ∃l. LTAKE n ll = SOME l ∧ toList ll = SOME l

⊢ ∀n f ll. LTAKE n (LMAP f ll) = OPTION_MAP (MAP f) (LTAKE n ll)

⊢ ∀n ll m l. LTAKE n ll = SOME l ∧ m < n ⇒ LNTH m ll = SOME l❲m❳

⊢ ∀x ll. ¬LFINITE ll ⇒ ∃l. LTAKE x ll = SOME l ∧ LPREFIX (fromList l) ll

⊢ LTAKE 0 (LUNFOLD f x) = SOME [] ∧
  LTAKE (SUC n) (LUNFOLD f x) =
  case f x of
    NONE => NONE
  | SOME (tx,hx) => OPTION_MAP (CONS hx) (LTAKE n (LUNFOLD f tx))

⊢ ∀m. LTAKE m [||] = NONE ⇔ 0 < m

⊢ ∀l m. LTAKE m [||] = SOME l ⇔ m = 0 ∧ l = []

⊢ ∀n ll.
    LTAKE (SUC n) ll =
    case LTAKE n ll of
      NONE => NONE
    | SOME l => case LNTH n ll of NONE => NONE | SOME e => SOME (l ⧺ [e])

⊢ LTAKE n ll = SOME l ∧ m ≤ n ⇒ LTAKE m ll = SOME (TAKE m l)

⊢ (∀l. LTAKE 0 l = SOME []) ∧ (∀n. LTAKE (SUC n) [||] = NONE) ∧
  ∀n h t. LTAKE (SUC n) (h:::t) = OPTION_MAP (CONS h) (LTAKE n t)

⊢ ∀P l. LTAKE_WHILE P l ++ₗ LDROP_WHILE P l = l

⊢ ∀l. LTAKE (LENGTH l) (fromList l) = SOME l

⊢ ∀n f. LTAKE n (fromSeq f) = SOME (GENLIST f n)

⊢ ∀ll. (LTL ll = NONE ⇔ ll = [||]) ∧ (NONE = LTL ll ⇔ ll = [||])

⊢ LTL_HD ll1 = LTL_HD ll2 ⇔ ll1 = ll2

⊢ LHD ll = OPTION_MAP SND (LTL_HD ll)

⊢ LTL_HD (h:::t) = SOME (t,h)

⊢ LTL_HD [||] = NONE

⊢ LTL_HD l = OPTION_BIND (LHD l) (λh. OPTION_BIND (LTL l) (λt. SOME (t,h)))

⊢ LTL_HD (LUNFOLD f x) = OPTION_MAP (LUNFOLD f ## I) (f x)

⊢ LTL ll = OPTION_MAP FST (LTL_HD ll)

⊢ (LTL_HD x = SOME (t,h) ⇔ x = h:::t) ∧ (LTL_HD x = NONE ⇔ x = [||])

⊢ LTL (l1 ++ₗ l2) =
  if l1 = [||] then LTL l2 else SOME (THE (LTL l1) ++ₗ l2)

⊢ LTL (h:::t) = SOME t

⊢ LTL (LGENLIST f limopt) =
  if limopt = SOME 0 then NONE
  else SOME (LGENLIST (f ∘ SUC) (OPTION_MAP PRE limopt))

⊢ LTL (LREPEAT l) = OPTION_MAP (λt. t ++ₗ LREPEAT l) (LTL (fromList l))

⊢ LTL (LUNFOLD f x) = OPTION_MAP (LUNFOLD f ∘ FST) (f x)

⊢ LTL [||] = NONE ∧ ∀h t. LTL (h:::t) = SOME t

⊢ LTL (fromList l) = if NULL l then NONE else SOME (fromList (TL l))

⊢ ∀f. LTL (fromSeq f) = SOME (fromSeq (f ∘ SUC))

⊢ ∀f x.
    LUNFOLD f x =
    case f x of NONE => [||] | SOME (v1,v2) => v2:::LUNFOLD f v1

⊢ ∀f1 f2 x1 x2.
    LUNFOLD f1 x1 = LUNFOLD f2 x2 ⇔
    ∃R. R x1 x2 ∧
        ∀y1 y2.
          R y1 y2 ⇒
          f1 y1 = NONE ∧ f2 y2 = NONE ∨
          ∃h t1 t2. f1 y1 = SOME (t1,h) ∧ f2 y2 = SOME (t2,h) ∧ R t1 t2

⊢ ∀R f s ll.
    R s ll ∧
    (∀s ll.
       R s ll ⇒
       f s = NONE ∧ ll = [||] ∨
       ∃s' x ll'.
         f s = SOME (s',x) ∧ LHD ll = SOME x ∧ LTL ll = SOME ll' ∧ R s' ll') ⇒
    LUNFOLD f s = ll

⊢ LUNFOLD LTL_HD ll = ll

⊢ ∀f x v1 v2.
    (f x = NONE ⇒ LUNFOLD f x = [||]) ∧
    (f x = SOME (v1,v2) ⇒ LUNFOLD f x = v2:::LUNFOLD f v1)

⊢ ∀f g.
    (∀x. g x = case f x of NONE => [||] | SOME (v1,v2) => v2:::g v1) ⇒
    ∀y. g y = LUNFOLD f y

⊢ ∀ll. LZIP (LUNZIP ll) = ll

⊢ ∀ll f. LFINITE ll ⇒ MAP f (THE (toList ll)) = THE (toList (LMAP f ll))

⊢ (∀x. P x ⇒ Q x) ⇒ every P l ⇒ every Q l

⊢ (∀x. P x ⇒ Q x) ⇒ exists P l ⇒ exists Q l

⊢ ∀ll1 ll2. ¬LFINITE ll1 ⇒ ll1 ++ₗ ll2 = ll1

⊢ ∀ll. ¬LFINITE ll ⇒ ∀n. ∃y. LDROP n ll = SOME y

⊢ ∀n l t. ¬LFINITE l ∧ LDROP n l = SOME t ⇒ ¬LFINITE t

⊢ ∀ll. ¬LFINITE ll ⇒ ∃f. ll = fromSeq f

⊢ ∀ll. ¬LFINITE ll ⇒ LLENGTH ll = NONE

⊢ ∀ll. ¬LFINITE ll ⇒ ∀n. ∃y. LTAKE n ll = SOME y

⊢ ∀ll. always P ll ⇒ always P (THE (LDROP k ll))

⊢ ∀P a0. always P a0 ⇔ ∃h t. a0 = h:::t ∧ P (h:::t) ∧ always P t

⊢ ∀P always'.
    (∀a0. always' a0 ⇒ ∃h t. a0 = h:::t ∧ P (h:::t) ∧ always' t) ⇒
    ∀a0. always' a0 ⇒ always P a0

⊢ ∀ll. always (λx. P x ∧ Q x) ll ⇒ always P ll

⊢ (∀ll. P ll ∨ ¬P ll ∧ Q (THE (LTL ll)) ⇒ Q ll) ⇒
  ∀ll. ll ≠ [||] ⇒ always (eventually P) ll ⇒ Q ll

⊢ ∀P h t. P (h:::t) ∧ always P t ⇒ always P (h:::t)

⊢ (always P [||] ⇔ F) ∧ ∀h t. always P (h:::t) ⇔ P (h:::t) ∧ always P t

⊢ ∀P a0. eventually P a0 ⇔ P a0 ∨ ∃h t. a0 = h:::t ∧ eventually P t

⊢ ∀P eventually'.
    (∀ll. P ll ⇒ eventually' ll) ∧
    (∀h t. eventually' t ⇒ eventually' (h:::t)) ⇒
    ∀a0. eventually P a0 ⇒ eventually' a0

⊢ ∀P. (∀ll. P ll ⇒ eventually P ll) ∧
      ∀h t. eventually P t ⇒ eventually P (h:::t)

⊢ ∀P eventually'.
    (∀ll. P ll ⇒ eventually' ll) ∧
    (∀h t. eventually P t ∧ eventually' t ⇒ eventually' (h:::t)) ⇒
    ∀a0. eventually P a0 ⇒ eventually' a0

⊢ (eventually P [||] ⇔ P [||]) ∧
  (eventually P (h:::t) ⇔ P (h:::t) ∨ eventually P t)

⊢ eventually P = until (K T) P

⊢ every P (l1 ++ₗ l2) ⇔ every P l1 ∧ (LFINITE l1 ⇒ every P l2)

⊢ ∀P ll1 ll2. every P (ll1 ++ₗ ll2) ⇒ every P ll1

⊢ ∀l P ll. LFINITE l ∧ every P (l ++ₗ ll) ⇒ every P ll

⊢ ∀f i ll1 ll2. every f ll1 ∧ LDROP i ll1 = SOME ll2 ⇒ every f ll2

⊢ ∀ll P. every P (LFILTER P ll)

⊢ ∀Q P ll. every Q ll ⇒ every Q (LFILTER P ll)

⊢ (every P (LGENLIST f (SOME n)) ⇔ ∀m. m < n ⇒ P (f m)) ∧
  (every P (LGENLIST f NONE) ⇔ ∀m. P (f m))

⊢ every P (LMAP f l) ⇔ every (P ∘ f) l

⊢ ∀P ll. every P ll ⇔ ∀n e. LNTH n ll = SOME e ⇒ P e

⊢ ∀P Q. (∀h t. Q (h:::t) ⇒ P h ∧ Q t) ⇒ ∀ll. Q ll ⇒ every P ll

⊢ ∀l P. every P (fromList l) ⇔ EVERY P l

⊢ ∀p f. every p (fromSeq f) ⇔ ∀i. p (f i)

⊢ ∀P Q.
    (∀h t. Q (h:::t) ⇒ P h) ∧ (∀h t. Q (h:::t) ⇒ Q t ∨ every P t) ⇒
    ∀ll. Q ll ⇒ every P ll

⊢ (every P [||] ⇔ T) ∧ (every P (h:::t) ⇔ P h ∧ every P t)

⊢ ∀l1 l2. exists P (l1 ++ₗ l2) ⇔ exists P l1 ∨ LFINITE l1 ∧ exists P l2

⊢ exists P (LFLATTEN ll) ⇔
  ∃p e0 s. LFINITE p ∧ every LFINITE p ∧ ll = p ++ₗ e0:::s ∧ exists P e0

⊢ exists P ll ⇔ ∃n a t. LDROP n ll = SOME (a:::t) ∧ P a

⊢ ∀l. exists P l ⇔ ∃n e. SOME e = LNTH n l ∧ P e

⊢ ∀P a0.
    exists P a0 ⇔ (∃h t. a0 = h:::t ∧ P h) ∨ ∃h t. a0 = h:::t ∧ exists P t

⊢ ∀p f. exists p (fromSeq f) ⇔ ∃i. p (f i)

⊢ ∀P exists'.
    (∀h t. P h ⇒ exists' (h:::t)) ∧ (∀h t. exists' t ⇒ exists' (h:::t)) ⇒
    ∀a0. exists P a0 ⇒ exists' a0

⊢ ∀P. (∀h t. P h ⇒ exists P (h:::t)) ∧ ∀h t. exists P t ⇒ exists P (h:::t)

⊢ ∀P Q.
    (∀h t. P h ⇒ Q (h:::t)) ∧ (∀h t. Q t ∧ exists P t ⇒ Q (h:::t)) ⇒
    ∀a0. exists P a0 ⇒ Q a0

⊢ ∀P exists'.
    (∀h t. P h ⇒ exists' (h:::t)) ∧
    (∀h t. exists P t ∧ exists' t ⇒ exists' (h:::t)) ⇒
    ∀a0. exists P a0 ⇒ exists' a0

⊢ (exists P [||] ⇔ F) ∧ (exists P (h:::t) ⇔ P h ∨ exists P t)

⊢ exists P ll ⇔
  ∃n a t l.
    LDROP n ll = SOME (a:::t) ∧ P a ∧ LTAKE n ll = SOME l ∧
    EVERY ($¬ ∘ P) l

⊢ ∀xs ys. fromList xs = fromList ys ⇔ xs = ys

⊢ fromList l = h:::t ⇔ ∃t0. l = h::t0 ∧ t = fromList t0

⊢ fromList l = [||] ⇔ l = []

⊢ ∀l f. fromList l ≠ fromSeq f

⊢ ∀ll. (∃l. ll = fromList l) ∨ ∃f. ll = fromSeq f

⊢ ∀f g. fromSeq f = fromSeq g ⇔ f = g

⊢ fromSeq f = f 0:::fromSeq (f ∘ SUC)

⊢ ∀l. toList (fromList l) = SOME l

⊢ ∀ll. ¬LFINITE ll ⇔ ∀n. ∃x. LNTH n ll = SOME x

⊢ LFINITE l1 ⇒ lbind (l1 ++ₗ l2) f = lbind l1 f ++ₗ lbind l2 f

⊢ lbind (h:::t) f = f h ++ₗ lbind t f

⊢ lbind ll f = h:::t ⇔
  ∃p e s t1 t2.
    ll = p ++ₗ e:::s ∧ LFINITE p ∧ (∀e0. e0 ∈ LSET p ⇒ f e0 = [||]) ∧
    t = t1 ++ₗ t2 ∧ f e = h:::t1 ∧ lbind s f = t2

⊢ lbind ll f = [||] ⇔ ∀e. e ∈ LSET ll ⇒ f e = [||]

⊢ let
    f b = if b then rpt_el T else [|F|];
    g b = if b then [||] else [|1|];
    bs = [|T; F|]
  in
    lbind bs (λb. lbind (f b) g) ≠ lbind (lbind bs f) g

⊢ lbind [||] f = [||] ∧ lbind (h:::t) f = f h ++ₗ lbind t f

⊢ ∀lo X.
    linear_order lo X ∧ finite_prefixes lo X ⇒
    ∃ll.
      X = {x | ∃i. LNTH i ll = SOME x} ∧
      lo ⊆ {(x,y) | ∃i j. i ≤ j ∧ LNTH i ll = SOME x ∧ LNTH j ll = SOME y} ∧
      ∀i j x. LNTH i ll = SOME x ∧ LNTH j ll = SOME x ⇒ i = j

⊢ ∀lo X.
    linear_order lo X ∧ finite_prefixes lo X ⇒
    ∃ll.
      X = {x | ∃i. LNTH i ll = SOME x} ∧
      lo = {(x,y) | ∃i j. i ≤ j ∧ LNTH i ll = SOME x ∧ LNTH j ll = SOME y} ∧
      ∀i j x. LNTH i ll = SOME x ∧ LNTH j ll = SOME x ⇒ i = j

⊢ ∀a0 a1.
    llength_rel a0 a1 ⇔
    a0 = [||] ∧ a1 = 0 ∨ ∃h n t. a0 = h:::t ∧ a1 = SUC n ∧ llength_rel t n

⊢ ∀llength_rel'.
    llength_rel' [||] 0 ∧
    (∀h n t. llength_rel' t n ⇒ llength_rel' (h:::t) (SUC n)) ⇒
    ∀a0 a1. llength_rel a0 a1 ⇒ llength_rel' a0 a1

⊢ llength_rel [||] 0 ∧
  ∀h n t. llength_rel t n ⇒ llength_rel (h:::t) (SUC n)

⊢ ∀llength_rel'.
    llength_rel' [||] 0 ∧
    (∀h n t.
       llength_rel t n ∧ llength_rel' t n ⇒ llength_rel' (h:::t) (SUC n)) ⇒
    ∀a0 a1. llength_rel a0 a1 ⇒ llength_rel' a0 a1

⊢ ∀f. ∃g.
    (∀x. LHD (g x) = OPTION_MAP SND (f x)) ∧
    ∀x. LTL (g x) = OPTION_MAP (g ∘ FST) (f x)

⊢ ∀f. ∃g. ∀x. g x = case f x of NONE => [||] | SOME (a,b) => b:::g a

⊢ ∀f. ∃!g. ∀x. g x = case f x of NONE => [||] | SOME (a,b) => b:::g a

⊢ ∀l. l = [||] ∨ ∃h t. l = h:::t

⊢ llist_CASE [||] b f = b ∧ llist_CASE (x:::ll) b f = f x ll

⊢ ∀P. (∀ll. P ll) ⇔ (∀l. P (fromList l)) ∧ ∀f. P (fromSeq f)

⊢ llist_rep (h:::t) = (λn. if n = 0 then SOME h else llist_rep t (n − 1))

⊢ llist_rep [||] = (λn. NONE)

⊢ ∀f. ∃!g.
    (∀x. LHD (g x) = OPTION_MAP SND (f x)) ∧
    ∀x. LTL (g x) = OPTION_MAP (g ∘ FST) (f x)

⊢ ∀R a0 a1.
    llist_upto R a0 a1 ⇔
    a1 = a0 ∨ R a0 a1 ∨ (∃y. llist_upto R a0 y ∧ llist_upto R y a1) ∨
    ∃x y z. a0 = z ++ₗ x ∧ a1 = z ++ₗ y ∧ llist_upto R x y

⊢ ∀R x y z. llist_upto R x y ⇒ llist_upto R (z ++ₗ x) (z ++ₗ y)

⊢ ∀R x. llist_upto R x x

⊢ ∀R llist_upto'.
    (∀x. llist_upto' x x) ∧ (∀x y. R x y ⇒ llist_upto' x y) ∧
    (∀x y z. llist_upto' x y ∧ llist_upto' y z ⇒ llist_upto' x z) ∧
    (∀x y z. llist_upto' x y ⇒ llist_upto' (z ++ₗ x) (z ++ₗ y)) ⇒
    ∀a0 a1. llist_upto R a0 a1 ⇒ llist_upto' a0 a1

⊢ ∀R x y. R x y ⇒ llist_upto R x y

⊢ ∀R. (∀x. llist_upto R x x) ∧ (∀x y. R x y ⇒ llist_upto R x y) ∧
      (∀x y z. llist_upto R x y ∧ llist_upto R y z ⇒ llist_upto R x z) ∧
      ∀x y z. llist_upto R x y ⇒ llist_upto R (z ++ₗ x) (z ++ₗ y)

⊢ ∀R llist_upto'.
    (∀x. llist_upto' x x) ∧ (∀x y. R x y ⇒ llist_upto' x y) ∧
    (∀x y z.
       llist_upto R x y ∧ llist_upto' x y ∧ llist_upto R y z ∧
       llist_upto' y z ⇒
       llist_upto' x z) ∧
    (∀x y z.
       llist_upto R x y ∧ llist_upto' x y ⇒ llist_upto' (z ++ₗ x) (z ++ₗ y)) ⇒
    ∀a0 a1. llist_upto R a0 a1 ⇒ llist_upto' a0 a1

⊢ ∀R x y z. llist_upto R x y ∧ llist_upto R y z ⇒ llist_upto R x z

⊢ ∀n l. n < LENGTH l ⇔ LNTH n (fromList l) = SOME l❲n❳

⊢ ∀ll x n1 n2. LNTH n1 ll = SOME x ∧ n2 ≤ n1 ⇒ ∃y. LNTH n2 ll = SOME y

⊢ lrep_ok (λn. FUNPOW (λm. OPTION_BIND m g) n fz)

⊢ lrep_ok (λn. OPTION_MAP f (g n)) ⇔ lrep_ok g

⊢ lrep_ok f ⇔ ∀n. IS_SOME (f (SUC n)) ⇒ IS_SOME (f n)

⊢ ∀a0.
    lrep_ok a0 ⇔
    a0 = (λn. NONE) ∨
    ∃h t. a0 = (λn. if n = 0 then SOME h else t (n − 1)) ∧ lrep_ok t

⊢ ∀lrep_ok'.
    (∀a0.
       lrep_ok' a0 ⇒
       a0 = (λn. NONE) ∨
       ∃h t. a0 = (λn. if n = 0 then SOME h else t (n − 1)) ∧ lrep_ok' t) ⇒
    ∀a0. lrep_ok' a0 ⇒ lrep_ok a0

⊢ lrep_ok (λn. NONE) ∧
  ∀h t. lrep_ok t ⇒ lrep_ok (λn. if n = 0 then SOME h else t (n − 1))

⊢ $¬ ∘ $¬ ∘ f = f ∧ $¬ ∘ $¬ = I

⊢ ∀mopt nopt.
    mopt = nopt ⇔
    ∃R. R mopt nopt ∧
        ∀m n.
          R m n ⇒
          m = SOME 0 ∧ n = SOME 0 ∨
          m ≠ SOME 0 ∧ n ≠ SOME 0 ∧ R (OPTION_MAP PRE m) (OPTION_MAP PRE n)

⊢ ∀ll l1 l2. LPREFIX l1 ll ∧ LPREFIX l2 ll ⇒ LPREFIX l1 l2 ∨ LPREFIX l2 l1

⊢ e:::rpt_el e = rpt_el e

⊢ rpt_el e = l1 ++ₗ l2 ⇔
  if LFINITE l1 then every ($= e) l1 ∧ l2 = rpt_el e else l1 = rpt_el e

⊢ toList (l1 ++ₗ l2) = SOME x ⇒ x = THE (toList l1) ⧺ THE (toList l2)

⊢ toList [||] = SOME [] ∧
  ∀h t. toList (h:::t) = OPTION_MAP (CONS h) (toList t)

⊢ ∀ll. LFINITE ll ⇒ fromList (THE (toList ll)) = ll

⊢ ∀P Q a0. until P Q a0 ⇔ Q a0 ∨ ∃h t. a0 = h:::t ∧ P (h:::t) ∧ until P Q t

⊢ ∀P Q until'.
    (∀ll. Q ll ⇒ until' ll) ∧ (∀h t. P (h:::t) ∧ until' t ⇒ until' (h:::t)) ⇒
    ∀a0. until P Q a0 ⇒ until' a0

⊢ ∀P Q.
    (∀ll. Q ll ⇒ until P Q ll) ∧
    ∀h t. P (h:::t) ∧ until P Q t ⇒ until P Q (h:::t)

⊢ ∀P Q until'.
    (∀ll. Q ll ⇒ until' ll) ∧
    (∀h t. P (h:::t) ∧ until P Q t ∧ until' t ⇒ until' (h:::t)) ⇒
    ∀a0. until P Q a0 ⇒ until' a0