feat(tactic/interactive/choose): nondependent choose (#3806)
Now you can write `choose!` to eliminate propositional arguments from the chosen functions.
```
example (h : ∀n m : ℕ, n < m → ∃i j, m = n + i ∨ m + j = n) : true :=
begin
choose! i j h using h,
guard_hyp i := ℕ → ℕ → ℕ,
guard_hyp j := ℕ → ℕ → ℕ,
guard_hyp h := ∀ (n m : ℕ), n < m → m = n + i n m ∨ m + j n m = n,
trivial
end
```
