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

import Base

# If a equals b, any property of a is also a property of b.
law subst:
  for -A: Type
  for -P: A -> Type
  for -a: A
  for -b: A
  for e: {a == b : A}
  for p: P(a)
  P(b)

Uses (0):