lean2/tests/lean/571.lean

8 lines
102 B
Text
Raw Permalink Normal View History

open nat
variables (P : → Prop)
example (H : ∃n, P n) : :=
begin
cases H with n p,
end