/- Verify that `deriving BEq` works on structures with `Prop`-fields.-/

structure S where
  foo : Nat
  p : True
  Bar : Nat
  deriving BEq

#eval (⟨1,⟨⟩,2⟩ : S) == ⟨1,⟨⟩,3⟩ -- false
#eval (⟨1,⟨⟩,2⟩ : S) == ⟨2,⟨⟩,2⟩ -- false
#eval (⟨1,⟨⟩,2⟩ : S) == ⟨1,⟨⟩,2⟩ -- true