~/jendhub

def AP.some_inj

bend-osdev-array@0.1.0.1 · PROOF.bend:1191

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base

1191def AP.some_inj(-T: Data, -x: T, -y: T, e: {Some{x} == Some{y} : Maybe<&2, T>}) -> {x == y : T}:
1192  Equal.cong(Maybe<&2, T>, T, m => AP.unsome(T, m, x), Some{x}, Some{y}, e)

Uses (3)

Used by (1)