~/jendhub

def h.eq_sym_f

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

import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
import Base

2375def h.eq_sym_f(
2376  ~K: Data, ~eq: K -> K -> Bool, ~refl: @x: K -> {eq(x, x) == True{} : Bool},
2377  ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K},
2378  +k: K, +key: K, e: {eq(k, key) == False{} : Bool}
2379) -> {eq(key, k) == False{} : Bool}:
2380  h.eq_sym_f.c(~K, ~eq, ~refl, ~sound, k, key, e, eq(key, k), {==})

Uses (2)

Used by (1)