law Equal.trans

Base · base.bend:546

import Base

546law Equal.trans:
547  for -A : Type
548  for -a : A
549  for -b : A
550  for -c : A
551  for ab : {a == b : A}
552  for bc : {b == c : A}
553  {a == c : A}

Uses (0)

This definition uses no other definition.

Used by (4090)