Equation1323 not implies Equation2744

@[equational_result]theorem Equation1323_not_implies_Equation2744 :    ∃ (G: Type) (_: Magma G), Equation1323 G ∧ ¬ Equation2744 G := by   let ⟨f, axiom3, hf⟩ := exists_complete_function seed  use G, ⟨op f⟩   constructor  · apply eq1323_if_conditions G _    apply op_RSy_LSy_eq_Id f    apply op_Ly_Ry_eq_LSy f axiom3  · by_contra h2744    apply Equation2744_left_injectivity at h2744    have : f seed1.lhs = f seed2.lhs := by      rw [hf seed1 (by simp [seed]), seed1]      rw [hf seed2 (by simp [seed]), seed2]    have : op f (.root (seed1.lhs).x) (.root (seed1.lhs).y) = op f (.root (1, a)) (.root (1, b')) := by      simpa [op, Relation.lhs.nonDiag, (by decide : a ≠ b')]    absurd h2744 (.root (1, a)) this    decide