~/jendhub

def pair_fst

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

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

95def pair_fst(-A: Type, -B: Type, a: A, b: B, c: A, d: B, e: {(a, b) == (c, d) : A & B}) -> {a == c : A}:
96  Equal.cong(A & B, A, p => Pair.fst(A, B, p), (a, b), (c, d), e)

Uses (4)

Used by (0)

No other definition uses this definition.