To prove an existential statement, one uses the tactic exists, supplying it with a so-called witness.
Existential statements can also occur among the assumptions. We will study this occurrence in a couple of weeks.
Created [07 Feb 2025]
Structural induction over Peano numbers
Specifications
Enter search terms or a module, class or function name.