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

import Base

law Equal.trans:
  for -A : Type
  for -a : A
  for -b : A
  for -c : A
  for ab : {a == b : A}
  for bc : {b == c : A}
  {a == c : A}

Uses (0):