def subst

lawful-arrays@0.1.0.0 · proof_base.bend:9

import lawful-arrays@0.1.0.0/proof_base.bend as ProofBase

import Base

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

Uses (0)

This definition uses no other definition.

Used by (112)