law Equal.cong

Base · base.bend:522

522law Equal.cong:
523  for -A: Type
524  for -B: Type
525  for -f: A -> B
526  for -a: A
527  for -b: A
528  for  e: {a == b : A}
529  {f(a) == f(b) : B}