Equal.trans3: law of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/equal.bend as Equal
Lines 37-47 of bend-mathlib@0.8.1.0/equal.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/equal.bend&start_line=37&end_line=47

import Base

# Equality chains through three steps: a = b, b = c and c = d give a = d.
law trans3:
  for -A: Type
  for -a: A
  for -b: A
  for -c: A
  for -d: A
  for ab: {a == b : A}
  for bc: {b == c : A}
  for cd: {c == d : A}
  {a == d : A}

Uses (0):