law cong2

bend-mathlib@0.8.1.0 · equal.bend:4

import Base

4# Applying a two-argument function to equal arguments gives equal results.
5law cong2:
6  for -A: Type
7  for -B: Type
8  for -C: Type
9  for -f: A -> B -> C
10  for -a1: A
11  for -a2: A
12  for -b1: B
13  for -b2: B
14  for ea: {a1 == a2 : A}
15  for eb: {b1 == b2 : B}
16  {f(a1, b1) == f(a2, b2) : C}