~/jendhub

law subst

bend-mathlib@0.8.1.0 · equal.bend:23

import bend-mathlib@0.8.1.0/equal.bend as Equal
import Base

23# If a equals b, any property of a is also a property of b.
24law subst:
25  for -A: Type
26  for -P: A -> Type
27  for -a: A
28  for -b: A
29  for e: {a == b : A}
30  for p: P(a)
31  P(b)

Uses (0)

This definition uses no other definition.

Used by (0)

No other definition uses this definition.