Equal.cong: law of Base
Import: import Base
Lines 522-529 of Base/base.bend: https://jend.leeeet.dev/read.txt?path=Base/base.bend&start_line=522&end_line=529

import Base

law Equal.cong:
  for -A: Type
  for -B: Type
  for -f: A -> B
  for -a: A
  for -b: A
  for  e: {a == b : A}
  {f(a) == f(b) : B}

Uses (0):