Theory update

⊢ LIST_UPDATE [] = I ∧
  ∀h t. LIST_UPDATE (h::t) = (FST h =+ SND h) ∘ LIST_UPDATE t

⊢ OVERRIDE =
  WFREC (@R. WF R ∧ ∀t x. R (FILTER (λy. FST x ≠ FST y) t) (x::t))
    (λOVERRIDE a.
         case a of
           [] => I []
         | x::t => I (x::OVERRIDE (FILTER (λy. FST x ≠ FST y) t)))

⊢ ∀f a. f⦇a ↦ f a⦈ = f

⊢ ∀f a b c. f⦇a ↦ b⦈ c = if a = c then b else f c

⊢ FIND P [] = NONE ∧ FIND P (h::t) = if P h then SOME h else FIND P t

⊢ ∀l1 l2.
    ALL_DISTINCT (MAP FST l2) ∧ PERM l1 l2 ⇒
    LIST_UPDATE l1 = LIST_UPDATE l2

⊢ ∀l f i.
    LIST_UPDATE l f i =
    case FIND (λx. FST x = i) l of NONE => f i | SOME (v1,e) => e

⊢ ∀l. LIST_UPDATE l = LIST_UPDATE (OVERRIDE l)

⊢ ∀R l. LIST_UPDATE l = LIST_UPDATE (QSORT R (OVERRIDE l))

⊢ ((∀l1 l2 r1 r2. (l1 =+ r1) ∘ (l2 =+ r2) = LIST_UPDATE [(l1,r1); (l2,r2)]) ∧
   (∀l r t. (l =+ r) ∘ LIST_UPDATE t = LIST_UPDATE ((l,r)::t)) ∧
   (∀l1 l2 r1 r2 f. f⦇l1 ↦ r1; l2 ↦ r2⦈ = LIST_UPDATE [(l1,r1); (l2,r2)] f) ∧
   ∀l r t f. (LIST_UPDATE t f)⦇l ↦ r⦈ = LIST_UPDATE ((l,r)::t) f) ∧
  (∀l1 l2. LIST_UPDATE l1 ∘ LIST_UPDATE l2 = LIST_UPDATE (l1 ⧺ l2)) ∧
  (∀l1 l2 r. LIST_UPDATE l1 ∘ (l2 =+ r) = LIST_UPDATE (SNOC (l2,r) l1)) ∧
  (∀l1 l2 f. LIST_UPDATE l1 (LIST_UPDATE l2 f) = LIST_UPDATE (l1 ⧺ l2) f) ∧
  ∀l1 l2 r f. LIST_UPDATE l1 f⦇l2 ↦ r⦈ = LIST_UPDATE (SNOC (l2,r) l1) f

⊢ OVERRIDE [] = [] ∧
  ∀x t. OVERRIDE (x::t) = x::OVERRIDE (FILTER (λy. FST x ≠ FST y) t)

⊢ ∀P. P [] ∧ (∀x t. P (FILTER (λy. FST x ≠ FST y) t) ⇒ P (x::t)) ⇒ ∀v. P v

⊢ ∀f1 f2 a b c. b ≠ c ⇒ f⦇a ↦ b⦈ ≠ f⦇a ↦ c⦈

⊢ ∀f a b. f a = b ⇔ f⦇a ↦ b⦈ = f

⊢ ∀f b a. f a = b ⇒ f⦇a ↦ b⦈ = f

⊢ ∀f a b c d. a ≠ b ⇒ f⦇a ↦ c; b ↦ d⦈ = f⦇b ↦ d; a ↦ c⦈

⊢ ∀f a b c. f⦇a ↦ c; a ↦ b⦈ = f⦇a ↦ c⦈

⊢ ∀a b. (a =+ b) = (λf c. if a = c then b else f c)