feat: add [recursor] attribute to Iff.elim

src/Init/Core.lean

@@ -760,6 +760,7 @@ def Or.symm := @Or.swap
 /- xor -/
 def Xor (a b : Prop) : Prop := (a ∧ ¬ b) ∨ (b ∧ ¬ a)
 
+@[recursor 5]
 theorem Iff.elim (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c :=
 Iff.rec h₁ h₂
 

tests/lean/run/induction1.lean

@@ -76,3 +76,9 @@ begin
   | nil       => exact rfl
   | cons z zs => exact absurd rfl (h z zs)
 end
+
+theorem tst10 {p q : Prop } (h₁ : p ↔ q) (h₂ : p) : q :=
+begin
+  induction h₁ using Iff.elim with
+  | _ h _ => exact h h₂
+end