Curry
Closed
Theorem & proof
·
curry.lean
·
✓ verified
1
2
3
import Mathlib theorem curry {p q r : Prop} (h : p ∧ q → r) : p → q → r :=fun hp hq => h ⟨hp, hq⟩
Rewards pledged
No rewards pledged yet.