def rw

bend-kit-collections@0.1.4.1 · PROOF.bend:552

import Base

552def rw(-A: Type, -P: A -> Type, -a: A, -b: A, e: {a == b : A}, p: P(b)) -> P(a):
553  %Equal.sym(A, a, b, e) : P(_)
554  p