ProofBase.subst: def of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/proof_base.bend as ProofBase
Lines 9-12 of lawful-arrays@0.1.0.0/proof_base.bend: https://jend.leeeet.dev/read.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&start_line=9&end_line=12

import Base

# Transport along an equation.
def subst(-A: Type, -P: A -> Type, -x: A, -y: A, e: {x == y : A}, p: P(x)) -> P(y):
  %e : P(_)
  p

Uses (0):