fix: remove [..] annotation from if simp theorems

fixes #1025

src/Init/Core.lean

@@ -409,28 +409,28 @@ instance {p q} [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
 
 /- if-then-else expression theorems -/
 
-theorem if_pos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
+theorem if_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
   match h with
   | isTrue  hc  => rfl
   | isFalse hnc => absurd hc hnc
 
-theorem if_neg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
+theorem if_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
   match h with
   | isTrue hc   => absurd hc hnc
   | isFalse hnc => rfl
 
-theorem dif_pos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = t hc :=
+theorem dif_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = t hc :=
   match h with
   | isTrue  hc  => rfl
   | isFalse hnc => absurd hc hnc
 
-theorem dif_neg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = e hnc :=
+theorem dif_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = e hnc :=
   match h with
   | isTrue hc   => absurd hc hnc
   | isFalse hnc => rfl
 
 -- Remark: dite and ite are "defally equal" when we ignore the proofs.
-theorem dif_eq_if (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) : dite c (fun h => t) (fun h => e) = ite c t e :=
+theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) : dite c (fun h => t) (fun h => e) = ite c t e :=
   match h with
   | isTrue hc   => rfl
   | isFalse hnc => rfl

tests/lean/run/1025.lean

@@ -0,0 +1,20 @@
+inductive Vector (α : Type u): Nat → Type u where
+| nil : Vector α 0
+| cons (head : α) (tail : Vector α n) : Vector α (n+1)
+
+namespace Vector
+  def mem (a : α) : Vector α n → Prop
+  | nil => False
+  | cons b l => a = b ∨ mem a l
+
+  def foldr (f : α → β → β) (init : β) : Vector α n → β
+  | nil     => init
+  | cons a l => f a (foldr f init l)
+
+  theorem foldr_max [LE β] [LT β] [DecidableRel (. < . : β → β → Prop)] {v: Vector α n} (f : α → β) (init : β)
+    (h: v.mem y):
+    f y ≤ v.foldr (λ x acc => max (f x) acc) init := by
+    induction v <;> simp only[foldr,max]
+    . admit
+    . split <;> admit
+end Vector