Logic.subst: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as Logic
Lines 106-109 of bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&start_line=106&end_line=109

import Base

# Transport a proof along an equation.
def subst(-A: Type, -P: A -> Type, -a: A, -b: A, e: {a == b : A}, pa: P(a)) -> P(b):
  %e : P(_)
  pa

Uses (0):