law is_eq_refl

bend-mathlib@0.8.1.0 · nat.bend:1266

import Base

1266# Every natural tests equal to itself.
1267law is_eq_refl:
1268  for n: Nat
1269  {Nat.is_eq(n, n) == True{} : Bool}