Proof.Equational

data a :~: b

type (:=:)

sym

trans

class Equality eq

class Preorder eq

reflexivity'

type a :\/: b

type a :/\: b

(=<=)

(=>=)

(=~=)

data Leibniz a b

data Reason eq x y

because

by

(===)

start

byDefinition

admitted

data Proxy t

cong

cong'

class Proposition f

type family xs :~> a :: *

class FromBool c

Conversion between equalities

fromRefl

fromLeibniz

reflToLeibniz

leibnizToRefl

Coercion

coerce

coerce'

Re-exported modules