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