theorem uncurry_prop

gabrieloak123 · Oct 14, 2023 · ef85bff · ef85bff
1 parent b80a7c4
commit ef85bff
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/src/logic.lean b/src/logic.lean
@@ -357,7 +357,12 @@ end
 theorem uncurry_prop :
   (P→(Q→R)) → ((P∧Q)→R)  :=
 begin
-  sorry,
+  intro h,
+  intro hpandq,
+  cases hpandq with hp hq,
+  apply h,
+  exact hp,
+  exact hq,
 end