Theorem: LoVe.hypothesis_example (LoVe/Lectures/LoVe08_Metaprogramming_Demo.lean)

State before:
α : Type
p : α → Prop
a : α
hpa : p a
⊢ p a
Tactic:
hypothesis
State after:
no goals