ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a b : Int<GOAL>-a = -b ↔ a = b
<VAR>a : Int<GOAL>-a = 0 ↔ a = 0
<VAR>a : Int<GOAL>-a ≠ 0 ↔ a ≠ 0
<VAR>i : Int<GOAL>i + -1 = i - 1
<VAR>m n : Nat<VAR>motive : Nat → Nat → Int → Prop<VAR>hp : ∀ (i n : Nat), motive (n + i) n ↑i<VAR>hn : ∀ (i m : Nat), motive m (m + i + 1) (Int.negSucc i)<GOAL>motive m n (Int.subNatNat m n)
<VAR>m n : Nat<GOAL>Int.subNatNat (m + n) m = ↑n
<VAR>m n : Nat<GOAL>Int.subNatNat m (m + n + 1) = Int.negSucc n
<VAR>m n k : Nat<GOAL>Int.subNatNat (m + k) (n + k) = Int.subNatNat m n
<VAR>m n : Nat<VAR>h : n ≤ m<GOAL>Int.subNatNat m n = ↑(m - n)
<VAR>m n : Nat<VAR>h : m < n<GOAL>Int.subNatNat m n = Int.negSucc (n - m).pred
<VAR>m n : Nat<VAR>h : m < n.succ<GOAL>Int.ofNat m + Int.negSucc n = Int.negSucc (n - m)
<VAR>n m : Nat<VAR>h : n ≤ m<VAR>k : Nat<GOAL>Int.subNatNat (m - n) k = Int.subNatNat m (k + n)
<VAR>m n k : Nat<GOAL>Int.subNatNat (m + n) k = ↑m + Int.subNatNat n k
<VAR>m n k : Nat<GOAL>Int.subNatNat m n + Int.negSucc k = Int.subNatNat m (n + k.succ)
<VAR>a b c : Int<GOAL>a + b + c = a + (b + c)
<VAR>m n k : Nat<GOAL>Int.negSucc m + Int.negSucc n + ↑k = Int.negSucc m + (Int.negSucc n + ↑k)
<VAR>m n : Nat<VAR>c : Int<GOAL>↑m + ↑n + c = ↑m + (↑n + c)
<VAR>a b c : Int<GOAL>a + (b + c) = b + (a + c)
<VAR>a b c : Int<GOAL>a + b + c = a + c + b
<VAR>n : Nat<GOAL>Int.subNatNat n n = 0
<VAR>a b : Int<VAR>h : a + b = 0<GOAL>-a = b
<VAR>a b : Int<VAR>h : a = -b<GOAL>b = -a
<VAR>a b : Int<GOAL>a = -b ↔ b = -a
<VAR>a b : Int<GOAL>-a = b ↔ -b = a
<VAR>a b : Int<GOAL>-a + (a + b) = b
<VAR>a b : Int<GOAL>a + (-a + b) = b
<VAR>a b c : Int<VAR>h : a + b = a + c<GOAL>b = c
<VAR>a b : Int<GOAL>-(a + b) = -a + -b
<VAR>n : Nat<GOAL>Int.negSucc n - 1 = Int.negSucc (n + 1)
<VAR>a b : Int<VAR>h : a = b<GOAL>a - b = 0
<VAR>a b : Int<VAR>h : a - b = 0<GOAL>a = b
<VAR>a b : Int<GOAL>a - b = 0 ↔ a = b
<VAR>a b c : Int<GOAL>a - b - c = a - (b + c)
<VAR>a b : Int<GOAL>-(a - b) = b - a
<VAR>a b : Int<GOAL>a - (a - b) = b
<VAR>a b c : Int<GOAL>a + b - c = a + (b - c)
<VAR>m n : Nat<VAR>h : m ≤ n<GOAL>↑(n - m) = ↑n - ↑m
<VAR>n : Nat<GOAL>Int.negSucc n = -↑n - 1
<VAR>m n : Nat<GOAL>Int.subNatNat m n = ↑m - ↑n
<VAR>m n : Nat<GOAL>(↑m - ↑n).toNat = m - n
<VAR>i j k : Int<GOAL>i + k = j + k ↔ i = j
<VAR>i j k : Int<GOAL>k + i = k + j ↔ i = j
<VAR>i j k : Int<GOAL>k - i = k - j ↔ i = j
<VAR>i j k : Int<GOAL>i - k = j - k ↔ i = j
<VAR>m n : Nat<GOAL>↑m * Int.negSucc n = -↑(m * n.succ)
<VAR>m n : Nat<GOAL>Int.negSucc m * ↑n = -↑(m.succ * n)
<VAR>m n : Nat<GOAL>Int.negSucc m * Int.negSucc n = ↑m.succ * ↑n.succ
<VAR>m n : Nat<GOAL>↑m * Int.negOfNat n = Int.negOfNat (m * n)
<VAR>m n : Nat<GOAL>Int.negOfNat m * ↑n = Int.negOfNat (m * n)
<VAR>m n : Nat<GOAL>Int.negSucc m * Int.negOfNat n = Int.ofNat (m.succ * n)
<VAR>m n : Nat<GOAL>Int.negOfNat n * Int.negSucc m = Int.ofNat (n * m.succ)
<VAR>a b c : Int<GOAL>a * b * c = a * (b * c)
<VAR>a b c : Int<GOAL>a * (b * c) = b * (a * c)
<VAR>a b c : Int<GOAL>a * b * c = a * c * b
<VAR>n : Nat<GOAL>Int.negOfNat n = Int.subNatNat 0 n
<VAR>m n k : Nat<GOAL>↑m * Int.subNatNat n k = Int.subNatNat (m * n) (m * k)
<VAR>m n : Nat<GOAL>Int.negOfNat m + Int.negOfNat n = Int.negOfNat (m + n)
<VAR>m n k : Nat<GOAL>Int.negSucc m * Int.subNatNat n k = Int.subNatNat (m.succ * k) (m.succ * n)
<VAR>a b c : Int<GOAL>a * (b + c) = a * b + a * c
<VAR>a b c : Int<GOAL>(a + b) * c = a * c + b * c
<VAR>a b : Int<GOAL>-(a * b) = -a * b
<VAR>a b : Int<GOAL>-(a * b) = a * -b
<VAR>a b : Int<GOAL>-a * b = -(a * b)
<VAR>a b : Int<GOAL>a * -b = -(a * b)
<VAR>a b : Int<GOAL>-a * -b = a * b
<VAR>a b : Int<GOAL>-a * b = a * -b
<VAR>a b c : Int<GOAL>a * (b - c) = a * b - a * c
<VAR>a b c : Int<GOAL>(a - b) * c = a * c - b * c
<VAR>a b : Int<GOAL>a * b = 0 ↔ a = 0 ∨ b = 0
<VAR>a b : Int<VAR>a0 : a ≠ 0<VAR>b0 : b ≠ 0<GOAL>a * b ≠ 0
<VAR>a b c : Int<VAR>ha : a ≠ 0<VAR>h : b * a = c * a<GOAL>b = c
<VAR>a b c : Int<VAR>ha : a ≠ 0<VAR>h : a * b = a * c<GOAL>b = c
<VAR>a b c : Int<VAR>h : c ≠ 0<GOAL>c * a = c * b ↔ a = b
<VAR>a b c : Int<VAR>h : c ≠ 0<GOAL>a * c = b * c ↔ a = b
<VAR>a b : Int<VAR>Hpos : a ≠ 0<VAR>H : b * a = a<GOAL>b = 1
<VAR>a b : Int<VAR>Hpos : b ≠ 0<VAR>H : b * a = b<GOAL>a = 1
<VAR>a b : Nat<GOAL>↑(a + b) = ↑a + ↑b
<VAR>a b : Nat<GOAL>↑(a * b) = ↑a * ↑b
<VAR>α : Type u<VAR>a : α<GOAL>(a :: List.nil).length = 1
<VAR>α : Type u_1<VAR>a : α<VAR>as : List α<GOAL>(a :: as).length = as.length + 1
<VAR>α : Type u<VAR>as : List α<VAR>i : Nat<VAR>a : α<GOAL>(as.set i a).length = as.length
<GOAL>∀ {α : Type u_1} {β : Type u_2} {f : α → β → α} {b : α}, List.foldl f b List.nil = b
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>f : β → α → β<VAR>l : List α<VAR>b : β<GOAL>List.foldl f b (a :: l) = List.foldl f (f b a) l
<VAR>α : Type u<VAR>as : List α<VAR>a : α<GOAL>(as.concat a).length = as.length + 1
<VAR>α : Type u<VAR>as bs : List α<VAR>a b : α<VAR>h : as.concat a = bs.concat b<GOAL>as = bs ∧ a = b
<VAR>α : Type u<VAR>eqv : α → α → Bool<GOAL>List.nil.isEqv List.nil eqv = true
<VAR>α : Type u<VAR>a : α<VAR>as : List α<VAR>eqv : α → α → Bool<GOAL>List.nil.isEqv (a :: as) eqv = false
<VAR>α : Type u<VAR>a : α<VAR>as : List α<VAR>eqv : α → α → Bool<GOAL>(a :: as).isEqv List.nil eqv = false
<GOAL>∀ {α : Type u_1} {a : α} {as : List α} {b : α} {bs : List α} {eqv : α → α → Bool}, (a :: as).isEqv (b :: bs) eqv = (eqv a b && as.isEqv bs eqv)
<VAR>α : Type u<VAR>n : Nat<GOAL>List.nil.get? n = none
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>(a :: l).get? 0 = some a
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>n : Nat<GOAL>(a :: l).get? (n + 1) = l.get? n
<VAR>α : Type u<VAR>l₁ l₂ : List α<GOAL>(∀ (n : Nat), l₁.get? n = l₂.get? n) → l₁ = l₂
<VAR>n : Nat<GOAL>∀ {α : Type u_1} {d : α}, List.nil.getD n d = d
<GOAL>∀ {α : Type u_1} {x : α} {xs : List α} {d : α}, (x :: xs).getD 0 d = x
<GOAL>∀ {α : Type u_1} {x : α} {xs : List α} {n : Nat} {d : α}, (x :: xs).getD (n + 1) d = xs.getD n d
<VAR>α : Type u<GOAL>List.nil.getLast? = none
<VAR>α : Type u<VAR>a : α<GOAL>List.nil.getLastD a = a
<VAR>α : Type u<VAR>a b : α<VAR>l : List α<GOAL>(b :: l).getLastD a = l.getLastD b
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>h : a :: l ≠ List.nil<GOAL>(a :: l).head h = a
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>(a :: l).head? = some a
<VAR>α : Type u<VAR>d : α<GOAL>List.nil.headD d = d
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>d : α<GOAL>(a :: l).headD d = a
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>(a :: l).tail? = some l
<VAR>α : Type u<VAR>l' : List α<GOAL>List.nil.tailD l' = l'
<VAR>α : Type u<VAR>a : α<VAR>l l' : List α<GOAL>(a :: l).tailD l' = l
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>List.map f List.nil = List.nil
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<VAR>l : List α<GOAL>List.map f (a :: l) = f a :: List.map f l
<VAR>α : Type u<VAR>p : α → Bool<GOAL>List.filter p List.nil = List.nil
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → Option β<GOAL>List.filterMap f List.nil = List.nil
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → Option β<VAR>a : α<VAR>l : List α<GOAL>List.filterMap f (a :: l) = match f a with | none => List.filterMap f l | some b => b :: List.filterMap f l
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1 → α_1} {b : α_1}, List.foldr f b List.nil = b
<VAR>α : Type u<VAR>a : α<GOAL>∀ {α_1 : Type u_1} {f : α → α_1 → α_1} {b : α_1} (l : List α), List.foldr f b (a :: l) = f a (List.foldr f b l)
<GOAL>∀ {α : Type u_1} {r : List α}, List.nil.reverseAux r = r
<GOAL>∀ {α : Type u_1} {a : α} {l r : List α}, (a :: l).reverseAux r = l.reverseAux (a :: r)
<VAR>α : Type u<GOAL>List.nil.reverse = List.nil
<VAR>α : Type u<VAR>as bs cs : List α<GOAL>(as.reverseAux bs).reverseAux cs = bs.reverseAux ((as.reverseAux List.nil).reverseAux cs)
<VAR>α : Type u<VAR>as bs : List α<GOAL>as.append bs = as ++ bs
<VAR>α : Type u<VAR>as : List α<GOAL>List.nil ++ as = as
<VAR>α : Type u<VAR>a : α<VAR>as bs : List α<GOAL>a :: as ++ bs = a :: (as ++ bs)
<VAR>α : Type u<VAR>as : List α<GOAL>as ++ List.nil = as
<VAR>α : Type u<VAR>as bs : List α<GOAL>(as ++ bs).length = as.length + bs.length
<VAR>α : Type u<VAR>as bs cs : List α<GOAL>as ++ bs ++ cs = as ++ (bs ++ cs)
<VAR>α : Type u<VAR>as : List α<VAR>b : α<VAR>bs : List α<GOAL>as ++ b :: bs = as ++ b :: List.nil ++ bs
<VAR>α : Type u<VAR>as : List α<VAR>a : α<GOAL>as.concat a = as ++ a :: List.nil
<VAR>α : Type u<VAR>as bs : List α<GOAL>as.reverseAux bs = as.reverseAux List.nil ++ bs
<VAR>α : Type u<VAR>a : α<VAR>as : List α<GOAL>(a :: as).reverse = as.reverse ++ a :: List.nil
<VAR>α : Type u<GOAL>List.nil.join = List.nil
<GOAL>∀ {α : Type u_1} {l : List α} {ls : List (List α)}, (l :: ls).join = l ++ ls.join
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → List β<GOAL>List.nil.bind f = List.nil
<VAR>α : Type u<VAR>β : Type v<VAR>x : α<VAR>xs : List α<VAR>f : α → List β<GOAL>(x :: xs).bind f = f x ++ xs.bind f
<GOAL>∀ {α : Type u_1} {a : α}, List.replicate 0 a = List.nil
<VAR>α : Type u<VAR>a : α<VAR>n : Nat<GOAL>List.replicate (n + 1) a = a :: List.replicate n a
<VAR>α : Type u<VAR>n : Nat<VAR>a : α<GOAL>(List.replicate n a).length = n
<VAR>α : Type u<VAR>x : α<VAR>xs : List α<GOAL>(x :: xs).isEmpty = false
<VAR>α : Type u<VAR>a : α<VAR>BEq α<GOAL>List.elem a List.nil = false
<VAR>α : Type u<VAR>b : α<VAR>bs : List α<VAR>BEq α<VAR>a : α<GOAL>List.elem a (b :: bs) = match a == b with | true => true | false => List.elem a bs
<VAR>α : Type u<VAR>a : α<VAR>BEq α<GOAL>List.nil.contains a = false
<VAR>α : Type u<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>as : List α<GOAL>List.elem a as = true → a ∈ as
<VAR>α : Type u<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>as : List α<VAR>h : a ∈ as<GOAL>List.elem a as = true
<VAR>α : Type u<VAR>a : α<VAR>as : List α<VAR>bs : List α<GOAL>a ∈ as → a ∈ as ++ bs
<VAR>α : Type u<VAR>b : α<VAR>bs : List α<VAR>as : List α<GOAL>b ∈ bs → b ∈ as ++ bs
<VAR>α : Type u<VAR>i : Nat<GOAL>List.take i List.nil = List.nil
<VAR>α : Type u<VAR>l : List α<GOAL>List.take 0 l = List.nil
<GOAL>∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.take (i + 1) (a :: as) = a :: List.take i as
<VAR>α : Type u<VAR>i : Nat<GOAL>List.drop i List.nil = List.nil
<VAR>α : Type u<VAR>l : List α<GOAL>List.drop 0 l = l
<GOAL>∀ {α : Type u_1} {a : α} {l : List α} {n : Nat}, List.drop (n + 1) (a :: l) = List.drop n l
<VAR>α : Type u<VAR>as : List α<VAR>i : Nat<VAR>h : as.length ≤ i<GOAL>List.drop i as = List.nil
<VAR>α : Type u<VAR>p : α → Bool<GOAL>List.takeWhile p List.nil = List.nil
<VAR>α : Type u<VAR>p : α → Bool<GOAL>List.dropWhile p List.nil = List.nil
<VAR>α : Type u<GOAL>List.nil.dropLast = List.nil
<GOAL>∀ {α : Type u_1} {x : α}, (x :: List.nil).dropLast = List.nil
<GOAL>∀ {α : Type u_1} {x y : α} {zs : List α}, (x :: y :: zs).dropLast = x :: (y :: zs).dropLast
<VAR>α : Type u<VAR>a : α<VAR>as : List α<GOAL>(a :: as).dropLast.length = as.length
<VAR>α : Type u<VAR>l : List α<VAR>BEq α<GOAL>List.nil.isPrefixOf l = true
<VAR>α : Type u<VAR>a : α<VAR>as : List α<VAR>BEq α<GOAL>(a :: as).isPrefixOf List.nil = false
<VAR>α : Type u<VAR>as : List α<VAR>b : α<VAR>bs : List α<VAR>BEq α<VAR>a : α<GOAL>(a :: as).isPrefixOf (b :: bs) = (a == b && as.isPrefixOf bs)
<VAR>α : Type u<VAR>l : List α<VAR>BEq α<GOAL>List.nil.isSuffixOf l = true
<VAR>α : Type u<VAR>n : Nat<GOAL>List.nil.rotateLeft n = List.nil
<VAR>α : Type u<VAR>n : Nat<GOAL>List.nil.rotateRight n = List.nil
<VAR>α : Type u<VAR>a b : α<VAR>BEq α<GOAL>List.nil.replace a b = List.nil
<VAR>α : Type u<VAR>as : List α<VAR>b c : α<VAR>BEq α<VAR>a : α<GOAL>(a :: as).replace b c = match b == a with | true => c :: as | false => a :: as.replace b c
<VAR>α : Type u<VAR>BEq α<VAR>a : α<GOAL>List.nil.erase a = List.nil
<VAR>α : Type u<VAR>BEq α<VAR>a b : α<VAR>l : List α<GOAL>(b :: l).erase a = ite ((b == a) = true) l (b :: l.erase a)
<VAR>α : Type u<VAR>i : Nat<GOAL>List.nil.eraseIdx i = List.nil
<GOAL>∀ {α : Type u_1} {a : α} {as : List α}, (a :: as).eraseIdx 0 = as
<GOAL>∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, (a :: as).eraseIdx (i + 1) = a :: as.eraseIdx i
<VAR>α : Type u<VAR>p : α → Bool<GOAL>List.find? p List.nil = none
<GOAL>∀ {α : Type u_1} {a : α} {as : List α} {p : α → Bool}, List.find? p (a :: as) = match p a with | true => some a | false => List.find? p as
<VAR>α : Type u<GOAL>∀ {α_1 : Type u_1} {f : α → Option α_1}, List.findSome? f List.nil = none
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>as : List α<VAR>f : α → Option β<GOAL>List.findSome? f (a :: as) = match f a with | some b => some b | none => List.findSome? f as
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>BEq α<GOAL>List.lookup a List.nil = none
<VAR>α : Type u<GOAL>∀ {β : Type u_1} {b : β} {es : List (α × β)} {a : α} [inst : BEq α] {k : α}, List.lookup a ({ fst := k, snd := b } :: es) = match a == k with | true => some b | false => List.lookup a es
<GOAL>∀ {α : Type u_1} {f : α → Bool}, List.nil.any f = false
<GOAL>∀ {α : Type u_1} {a : α} {l : List α} {f : α → Bool}, (a :: l).any f = (f a || l.any f)
<GOAL>∀ {α : Type u_1} {f : α → Bool}, List.nil.all f = true
<GOAL>∀ {α : Type u_1} {a : α} {l : List α} {f : α → Bool}, (a :: l).all f = (f a && l.all f)
<VAR>a : Bool<VAR>l : List Bool<GOAL>(a :: l).or = (a || l.or)
<VAR>a : Bool<VAR>l : List Bool<GOAL>(a :: l).and = (a && l.and)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List β<VAR>f : α → β → γ<GOAL>List.zipWith f List.nil l = List.nil
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<VAR>f : α → β → γ<GOAL>List.zipWith f l List.nil = List.nil
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>as : List α<VAR>b : β<VAR>bs : List β<VAR>f : α → β → γ<GOAL>List.zipWith f (a :: as) (b :: bs) = f a b :: List.zipWith f as bs
<VAR>α : Type u<VAR>β : Type v<VAR>l : List β<GOAL>List.nil.zip l = List.nil
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<GOAL>l.zip List.nil = List.nil
<GOAL>∀ {α : Type u_1} {a : α} {as : List α} {α_1 : Type u_2} {b : α_1} {bs : List α_1}, (a :: as).zip (b :: bs) = { fst := a, snd := b } :: as.zip bs
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {as : List α}, List.zipWithAll f as List.nil = List.map (fun a => f (some a) none) as
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {bs : List α_1}, List.zipWithAll f List.nil bs = List.map (fun b => f none (some b)) bs
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {a : α} {as : List α} {b : α_1} {bs : List α_1}, List.zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: List.zipWithAll f as bs
<VAR>α : Type u<VAR>β : Type v<GOAL>List.nil.unzip = { fst := List.nil, snd := List.nil }
<VAR>α : Type u<VAR>β : Type v<VAR>t : List (α × β)<VAR>h : α × β<GOAL>(h :: t).unzip = match t.unzip with | { fst := al, snd := bl } => { fst := h.fst :: al, snd := h.snd :: bl }
<VAR>i : Nat<GOAL>List.iota (i + 1) = (i + 1) :: List.iota i
<VAR>α : Type u<VAR>i : Nat<GOAL>List.enumFrom i List.nil = List.nil
<GOAL>∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.enumFrom i (a :: as) = { fst := i, snd := a } :: List.enumFrom (i + 1) as
<VAR>α : Type u<GOAL>List.nil.enum = List.nil
<VAR>α : Type u<VAR>sep : α<GOAL>List.intersperse sep List.nil = List.nil
<VAR>α : Type u<VAR>x : α<VAR>sep : α<GOAL>List.intersperse sep (x :: List.nil) = x :: List.nil
<VAR>α : Type u<VAR>x y : α<VAR>zs : List α<VAR>sep : α<GOAL>List.intersperse sep (x :: y :: zs) = x :: sep :: List.intersperse sep (y :: zs)
<VAR>b : Bool<GOAL>b = true ∨ b = false
<VAR>b : Bool<GOAL>b = false ↔ b ≠ true
<VAR>b : Bool<GOAL>b ≠ false ↔ b = true
<VAR>a b : Bool<GOAL>a = b ↔ (a = true ↔ b = true)
<VAR>b : Bool<VAR>Decidable (b = true)<GOAL>decide (b = true) = b
<VAR>b : Bool<VAR>Decidable (b = false)<GOAL>decide (b = false) = !b
<VAR>b : Bool<VAR>Decidable (true = b)<GOAL>decide (true = b) = b
<VAR>b : Bool<VAR>Decidable (false = b)<GOAL>decide (false = b) = !b
<VAR>a b : Bool<GOAL>(a && (a && b)) = (a && b)
<VAR>a b : Bool<GOAL>(a && b && b) = (a && b)
<VAR>b : Bool<GOAL>b = true ∧ b = false ↔ False
<VAR>b : Bool<GOAL>b = false ∧ b = true ↔ False
<VAR>x y : Bool<GOAL>(x && y) = (y && x)
<VAR>x y z : Bool<GOAL>(x && (y && z)) = (y && (x && z))
<VAR>x y z : Bool<GOAL>(x && y && z) = (x && z && y)
<VAR>a b : Bool<GOAL>(a && b) = a ↔ a = true → b = true
<VAR>a b : Bool<GOAL>(a && b) = b ↔ b = true → a = true
<VAR>a b : Bool<GOAL>a = (a && b) ↔ a = true → b = true
<VAR>a b : Bool<GOAL>b = (a && b) ↔ b = true → a = true
<VAR>a b : Bool<GOAL>(a || (a || b)) = (a || b)
<VAR>a b : Bool<GOAL>(a || b || b) = (a || b)
<VAR>b : Bool<GOAL>b = true ∨ b = false ↔ True
<VAR>b : Bool<GOAL>b = false ∨ b = true ↔ True
<VAR>a b : Bool<GOAL>(a || b) = a ↔ b = true → a = true
<VAR>a b : Bool<GOAL>(a || b) = b ↔ a = true → b = true
<VAR>a b : Bool<GOAL>a = (a || b) ↔ b = true → a = true
<VAR>a b : Bool<GOAL>b = (a || b) ↔ a = true → b = true
<VAR>x y : Bool<GOAL>(x || y) = (y || x)
<VAR>x y z : Bool<GOAL>(x || (y || z)) = (y || (x || z))
<VAR>x y z : Bool<GOAL>(x || y || z) = (x || z || y)
<VAR>x y z : Bool<GOAL>(x && (y || z)) = (x && y || x && z)
<VAR>x y z : Bool<GOAL>((x || y) && z) = (x && z || y && z)
<VAR>x y z : Bool<GOAL>(x || y && z) = ((x || y) && (x || z))
<VAR>x y z : Bool<GOAL>(x && y || z) = ((x || z) && (y || z))
<VAR>x y z : Bool<GOAL>(x && xor y z) = xor (x && y) (x && z)
<VAR>x y z : Bool<GOAL>(xor x y && z) = xor (x && z) (y && z)
<VAR>x y : Bool<GOAL>(!(x && y)) = (!x || !y)
<VAR>x y : Bool<GOAL>(!(x || y)) = (!x && !y)
<VAR>x y : Bool<GOAL>(x && y) = true ↔ x = true ∧ y = true
<VAR>x y : Bool<GOAL>(x && y) = false ↔ x = false ∨ y = false
<VAR>x y : Bool<GOAL>(x && y) = false ↔ x = true → y = false
<VAR>x y : Bool<GOAL>(x || y) = true ↔ x = true ∨ y = true
<VAR>x y : Bool<GOAL>(x || y) = false ↔ x = false ∧ y = false
<VAR>b : Bool<GOAL>(false = b) = (b = false)
<VAR>b : Bool<GOAL>(true = b) = (b = true)
<VAR>b : Bool<GOAL>(!b) = b ↔ False
<VAR>a b : Bool<GOAL>(a == (a == b)) = b
<VAR>a b : Bool<GOAL>((a == b) == b) = a
<VAR>a b : Bool<GOAL>(a != (a != b)) = b
<VAR>a b : Bool<GOAL>((a != b) != b) = a
<VAR>x y : Bool<GOAL>((!x) != !y) = (x != y)
<VAR>x y z : Bool<GOAL>((x != y) != z) = (x != (y != z))
<VAR>x y z : Bool<GOAL>(x != y) = (x != z) ↔ y = z
<VAR>x y z : Bool<GOAL>(x != z) = (y != z) ↔ x = y
<VAR>x y : Bool<GOAL>x ≠ y → x = !y
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>DecidableEq α<VAR>a b : α<GOAL>(a == b) = decide (a = b)
<VAR>a b : Bool<GOAL>¬a = !b ↔ a = b
<VAR>a b : Bool<GOAL>¬(!a) = b ↔ a = b
<VAR>a b : Bool<GOAL>(a = true ↔ b = true) ↔ a = b
<VAR>a b : Bool<GOAL>(a = true ↔ b = false) ↔ a = !b
<VAR>a b : Bool<GOAL>(a = false ↔ b = true) ↔ (!a) = b
<VAR>a b : Bool<GOAL>(a = false ↔ b = false) ↔ (!a) = !b
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<GOAL>(a == b) = (b == a)
<VAR>x y : Bool<GOAL>xor (!x) y = !xor x y
<VAR>x y : Bool<GOAL>(xor x !y) = !xor x y
<VAR>x y : Bool<GOAL>(xor (!x) !y) = xor x y
<VAR>x y : Bool<GOAL>xor x y = xor y x
<VAR>x y z : Bool<GOAL>xor x (xor y z) = xor y (xor x z)
<VAR>x y z : Bool<GOAL>xor (xor x y) z = xor (xor x z) y
<VAR>x y z : Bool<GOAL>xor (xor x y) z = xor x (xor y z)
<VAR>x y z : Bool<GOAL>xor x y = xor x z ↔ y = z
<VAR>x y z : Bool<GOAL>xor x z = xor y z ↔ x = y
<VAR>x y z : Bool<GOAL>x ≤ y → y ≤ z → x ≤ z
<VAR>x y : Bool<GOAL>x ≤ y → y ≤ x → x = y
<VAR>x y : Bool<GOAL>x ≤ y ∨ y ≤ x
<VAR>x y : Bool<GOAL>x < y → ¬y < x
<VAR>x y z : Bool<GOAL>x < y → y < z → x < z
<VAR>x y : Bool<GOAL>x < y ↔ x ≤ y ∧ ¬y ≤ x
<VAR>x y z : Bool<GOAL>x ≤ y → y < z → x < z
<VAR>x y z : Bool<GOAL>x < y → y ≤ z → x < z
<VAR>x y : Bool<GOAL>x < y → x ≤ y
<VAR>x y : Bool<GOAL>x = y → x ≤ y
<VAR>x y : Bool<GOAL>x < y → x ≠ y
<VAR>x y : Bool<GOAL>x ≤ y → x ≠ y → x < y
<VAR>x y : Bool<GOAL>x < y ∨ x = y → x ≤ y
<VAR>x : Bool<GOAL>true ≤ x → x = true
<VAR>x : Bool<GOAL>x ≤ false → x = false
<VAR>x y : Bool<GOAL>(!x) = !y → x = y
<VAR>x y : Bool<GOAL>(!x) = !y ↔ x = y
<VAR>m x y : Bool<GOAL>(x && m) = (y && m) → (x || m) = (y || m) → x = y
<VAR>m x y : Bool<GOAL>(x && m) = (y && m) ∧ (x || m) = (y || m) ↔ x = y
<VAR>m x y : Bool<GOAL>(m && x) = (m && y) → (m || x) = (m || y) → x = y
<VAR>m x y : Bool<GOAL>(m && x) = (m && y) ∧ (m || x) = (m || y) ↔ x = y
<VAR>c : Bool<GOAL>c.toNat ≤ 1
<VAR>b : Bool<GOAL>b.toNat = 0 ↔ b = false
<VAR>b : Bool<GOAL>b.toNat = 1 ↔ b = true
<VAR>p : Prop<VAR>h : Decidable p<VAR>f : Bool<GOAL>(if p then true else f) = (decide p || f)
<VAR>p : Prop<VAR>h : Decidable p<VAR>f : Bool<GOAL>(if p then false else f) = (!decide p && f)
<VAR>p : Prop<VAR>h : Decidable p<VAR>t : Bool<GOAL>(if p then t else true) = (!decide p || t)
<VAR>p : Prop<VAR>h : Decidable p<VAR>t : Bool<GOAL>(if p then t else false) = (decide p && t)
<VAR>p : Prop<VAR>h : Decidable p<VAR>t f : Bool<GOAL>((if p then t else f) = true) = if p then t = true else f = true
<VAR>p : Prop<VAR>h : Decidable p<VAR>t f : Bool<GOAL>((if p then t else f) = false) = if p then t = false else f = false
<VAR>p : Prop<VAR>h : Decidable p<VAR>b c : Bool<GOAL>(¬if p then b = true else c = true) ↔ if p then b = false else c = false
<VAR>p : Prop<VAR>h : Decidable p<VAR>b c : Bool<GOAL>(¬if p then b = false else c = false) ↔ if p then b = true else c = true
<VAR>p : Prop<VAR>h : Decidable p<VAR>b c : Bool<GOAL>(¬if p then b = true else c = false) ↔ if p then b = false else c = true
<VAR>p : Prop<VAR>h : Decidable p<VAR>b c : Bool<GOAL>(¬if p then b = false else c = true) ↔ if p then b = true else c = false
<VAR>b : Bool<GOAL>b = false → b = true ↔ b = true
<VAR>b : Bool<GOAL>b = true → b = false ↔ b = false
<VAR>α : Type u_1<VAR>b : Bool<VAR>t e : α<GOAL>(bif b then t else e) = if b = true then t else e
<VAR>b : Bool<GOAL>∀ {α : Type u_1} {x y : α}, (bif b then x else y) = if b = true then x else y
<VAR>α : Type u_1<VAR>b : Bool<VAR>t e : α<GOAL>(bif !b then t else e) = bif b then e else t
<VAR>α : Type u_1<VAR>c : Bool<VAR>t : α<GOAL>(bif c then t else t) = t
<VAR>α : Type u_1<VAR>p : Prop<VAR>Decidable p<VAR>t e : α<GOAL>(bif decide p then t else e) = if p then t else e
<VAR>α : Type u_1<VAR>a : Bool<VAR>p : Prop<VAR>h : Decidable p<VAR>x y u v : α<GOAL>((bif a then x else y) = if p then u else v) ↔ (if a = true then x else y) = if p then u else v
<VAR>α : Type u_1<VAR>p : Prop<VAR>h : Decidable p<VAR>a : Bool<VAR>x y u v : α<GOAL>((if p then x else y) = bif a then u else v) ↔ (if p then x else y) = if a = true then u else v
<VAR>c t f : Bool<GOAL>((bif c then t else f) = true) = if c = true then t = true else f = true
<VAR>c t f : Bool<GOAL>((bif c then t else f) = false) = if c = true then t = false else f = false
<VAR>α : Type u<VAR>a b : α<GOAL>(bif true then a else b) = a
<VAR>α : Type u<VAR>a b : α<GOAL>(bif false then a else b) = b
<VAR>c f : Bool<GOAL>(bif c then true else f) = (c || f)
<VAR>c f : Bool<GOAL>(bif c then false else f) = (!c && f)
<VAR>c t : Bool<GOAL>(bif c then t else true) = (!c || t)
<VAR>c t : Bool<GOAL>(bif c then t else false) = (c && t)
<VAR>c b : Bool<GOAL>(bif c then c else b) = (c || b)
<VAR>c b : Bool<GOAL>(bif c then b else c) = (c && b)
<VAR>p q : Prop<VAR>dpq : Decidable (p ∧ q)<VAR>dp : Decidable p<VAR>dq : Decidable q<GOAL>decide (p ∧ q) = (decide p && decide q)
<VAR>p q : Prop<VAR>dpq : Decidable (p ∨ q)<VAR>dp : Decidable p<VAR>dq : Decidable q<GOAL>decide (p ∨ q) = (decide p || decide q)
<VAR>p q : Prop<VAR>dpq : Decidable (p ↔ q)<VAR>dp : Decidable p<VAR>dq : Decidable q<GOAL>decide (p ↔ q) = (decide p == decide q)
<VAR>p : Prop<VAR>h : Decidable p<GOAL>false = decide p ↔ ¬p
<VAR>p : Prop<VAR>h : Decidable p<GOAL>true = decide p ↔ p
<VAR>α : Type u_1<VAR>as : List α<VAR>n : Nat<GOAL>as.length + n = as.lengthTRAux n
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<VAR>acc : Array α<VAR>xs : List α<VAR>n : Nat<GOAL>l = acc.data ++ xs → List.setTR.go l a xs n acc = acc.data ++ xs.set n a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>as : List α<VAR>bs : List β<GOAL>List.mapTR.loop f as bs = bs.reverse ++ List.map f as
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>as bs : List α<GOAL>List.filterTR.loop p as bs = bs.reverse ++ List.filter p as
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>f : α → Option β<VAR>as : List α<VAR>acc : Array β<GOAL>List.filterMapTR.go f as acc = acc.data ++ List.filterMap f as
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>f : α → List β<VAR>as : List α<VAR>acc : Array β<GOAL>List.bindTR.go f as acc = acc.data ++ as.bind f
<VAR>α : Type u_1<VAR>a : α<VAR>m n : Nat<GOAL>List.replicateTR.loop a n (List.replicate m a) = List.replicate (n + m) a