Equal.cong2: law of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/equal.bend as Equal
Lines 4-16 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=4&end_line=16

import Base

# Applying a two-argument function to equal arguments gives equal results.
law cong2:
  for -A: Type
  for -B: Type
  for -C: Type
  for -f: A -> B -> C
  for -a1: A
  for -a2: A
  for -b1: B
  for -b2: B
  for ea: {a1 == a2 : A}
  for eb: {b1 == b2 : B}
  {f(a1, b1) == f(a2, b2) : C}

Uses (0):