diff --git a/coq/src/putnam_1996_a4.v b/coq/src/putnam_1996_a4.v
index d7f832ea..f1ccd011 100644
--- a/coq/src/putnam_1996_a4.v
+++ b/coq/src/putnam_1996_a4.v
@@ -5,7 +5,7 @@ Theorem putnam_1996_a4
     (SS : Ensemble (A * A * A))
     (hSdistinct: forall a b c : A, In _ SS (a, b, c) -> a <> b /\ b <> c /\ c <> a)
     (hS1 : forall a b c : A, In _ SS (a, b, c) <-> In _ SS (b, c, a))
-    (hS2 : forall a b c : A, In _ SS (a, b, c) <-> ~ (In _ SS (c, b, a)))
+    (hS2 : forall a b c : A, a <> c -> (In _ SS (a, b, c) <-> ~ (In _ SS (c, b, a))))
     (hS3 : forall a b c d : A, (In _ SS (a, b, c) /\ In _ SS (c, d, a)) <-> (In _ SS (b, c, d) /\ In _ SS (d, a, b)))
     : exists g : A -> R, Injective g /\ (forall a b c : A, g a < g b /\ g b < g c -> In _ SS (a, b, c)).
 Proof. Admitted.
diff --git a/isabelle/putnam_1996_a4.thy b/isabelle/putnam_1996_a4.thy
index 5b947aeb..6ad1eb6e 100644
--- a/isabelle/putnam_1996_a4.thy
+++ b/isabelle/putnam_1996_a4.thy
@@ -9,7 +9,7 @@ theorem putnam_1996_a4:
   assumes hA : "CARD('A) = n"
     and hSdistinct: "\<forall>a b c::'A. ((a, b, c) \<in> S \<longrightarrow> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c))"
     and hS1 : " \<forall> a b c :: 'A. (a, b, c) \<in> S \<longleftrightarrow> (b, c, a) \<in> S"
-    and hS2 : " \<forall> a b c :: 'A. (a, b, c) \<in> S \<longleftrightarrow> (c, b, a) \<notin> S"
+    and hS2 : " \<forall> a b c :: 'A. a \<noteq> c \<longrightarrow> ((a, b, c) \<in> S \<longleftrightarrow> (c, b, a) \<notin> S)"
     and hS3 : " \<forall> a b c d :: 'A. ((a, b, c) \<in> S \<and> (c, d, a) \<in> S) \<longleftrightarrow> ((b, c, d) \<in> S \<and> (d, a, b) \<in> S)"
   shows "\<exists> g :: 'A \<Rightarrow> real. inj g \<and> (\<forall> a b c :: 'A. (g a < g b \<and> g b < g c) \<longrightarrow> (a, b, c) \<in> S)"
   sorry
diff --git a/lean4/src/putnam_1996_a4.lean b/lean4/src/putnam_1996_a4.lean
index c3771b9e..3bc3877e 100644
--- a/lean4/src/putnam_1996_a4.lean
+++ b/lean4/src/putnam_1996_a4.lean
@@ -12,7 +12,7 @@ theorem putnam_1996_a4
 (S : Set (A × A × A))
 (hSdistinct : ∀ a b c : A, ⟨a, b, c⟩ ∈ S → a ≠ b ∧ b ≠ c ∧ a ≠ c)
 (hS1 : ∀ a b c : A, ⟨a, b, c⟩ ∈ S ↔ ⟨b, c, a⟩ ∈ S)
-(hS2 : ∀ a b c : A, ⟨a, b, c⟩ ∈ S ↔ ⟨c, b, a⟩ ∉ S)
+(hS2 : ∀ a b c : A, a ≠ c → (⟨a, b, c⟩ ∈ S ↔ ⟨c, b, a⟩ ∉ S))
 (hS3 : ∀ a b c d : A, (⟨a, b, c⟩ ∈ S ∧ ⟨c, d, a⟩ ∈ S) ↔ (⟨b,c,d⟩ ∈ S ∧ ⟨d,a,b⟩ ∈ S))
 : ∃ g : A → ℝ, Injective g ∧ (∀ a b c : A, g a < g b ∧ g b < g c → ⟨a,b,c⟩ ∈ S) :=
 sorry