Checking logical equivalence of two theorems

Stream: Is there code for X?

[clijo]

If I have two theorems like:

theorem Thm1 (arg₁ : Type₁) (arg₂ : Type₂) ... : Prop1 := by sorry
theorem Thm2 (arg₁ : Type₁) (arg₂ : Type₂) ... : Prop2 := by sorry

is there code to check whether they are logically equivalent propositions?

Consider for instance the pair:

theorem Thm1 (x y c : ℝ) (h1 : c > 0) (h2 : x > y) : x*c > c*y := by sorry
theorem Thm2 (x y c : ℝ) (h1 : c > 0) (h2 : x > y) : x*(-c) < y*(-c) := by sorry

[Kim Morrison]

In general, this is as hard as all mathematics.

[Kim Morrison]

You'll need to restrict scope somewhat before anything automatic can help.

[Kim Morrison]

import Mathlib

def Thm1 (x y c : ℝ) (h1 : c > 0) (h2 : x > y) : Prop := x*c > c*y
def Thm2 (x y c : ℝ) (h1 : c > 0) (h2 : x > y) : Prop := x*(-c) < y*(-c)

example : Thm1 x y c h1 h2 ↔ Thm2 x y c h1 h2 := by grind [Thm1, Thm2]

etc