law trans3

bend-mathlib@0.8.1.0 · equal.bend:37

import Base

37# Equality chains through three steps: a = b, b = c and c = d give a = d.
38law trans3:
39  for -A: Type
40  for -a: A
41  for -b: A
42  for -c: A
43  for -d: A
44  for ab: {a == b : A}
45  for bc: {b == c : A}
46  for cd: {c == d : A}
47  {a == d : A}