Theorem: testSuccess (playground/tactic.lean)

State before:
⊢ Nat → ∀ (bint : Int), Nat → ∀ (dint : Int), Int → bint = dint
Tactic:
intros a b c d e
State after:
a : Nat
b : Int
c : Nat
d e : Int
⊢ b = d