law cong_succ

bend-mathlib@0.8.1.0 · equal.bend:54

import Base

54# Equal naturals have equal successors.
55law cong_succ:
56  for -a: Nat
57  for -b: Nat
58  for e: {a == b : Nat}
59  {1n+a == 1n+b : Nat}