law is_eq_refl_sym

bend-mathlib@0.8.1.0 · nat.bend:4239

import Base

4239# Every natural tests equal to itself, reversed to rewrite toward the simple side.
4240law is_eq_refl_sym:
4241  for n: Nat
4242  {True{} == Nat.is_eq(n, n) : Bool}