berberman

universe u v

inductive Eq' {α : Sort u} : α → α → Sort (max u 1) where
  | refl (x : α) : Eq' x x

infix:50 " ≡ " => Eq'

def Eq'.rfl {α : Sort u} {x : α} : x ≡ x := refl x

noncomputable def Eq'.subst {α : Sort u}