def subst

bend-collections-laws-math@1.0.0.0 · proofs/lib/logic.bend:106

import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as Logic

import Base

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

Uses (0)

This definition uses no other definition.

Used by (540)