Boolean equality

class PartialEquivBEq (α : Type u_1) [BEq α] : Prop

PartialEquivBEq α says that the BEq implementation is a partial equivalence relation, that is:

• it is symmetric: a == b → b == a
• it is transitive: a == b → b == c → a == c.

• symm : ∀ {a b : α}, (a == b) = true → (b == a) = true

  Symmetry for BEq. If a == b then b == a.

• trans : ∀ {a b c : α}, (a == b) = true → (b == c) = true → (a == c) = true

  Transitivity for BEq. If a == b and b == c then a == c.

theorem PartialEquivBEq.symm {α : Type u_1} [BEq α] [self : PartialEquivBEq α] {a : α} {b : α} : (a == b) = true → (b == a) = true

Symmetry for BEq. If a == b then b == a.

theorem PartialEquivBEq.trans {α : Type u_1} [BEq α] [self : PartialEquivBEq α] {a : α} {b : α} {c : α} : (a == b) = true → (b == c) = true → (a == c) = true

Transitivity for BEq. If a == b and b == c then a == c.