def h.eq_sym_f.c

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

import Base

2361# eq is symmetric on False, given refl and sound.
2362def h.eq_sym_f.c(
2363  ~K: Data, ~eq: K -> K -> Bool, ~refl: @x: K -> {eq(x, x) == True{} : Bool},
2364  ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K},
2365  +k: K, +key: K, e: {eq(k, key) == False{} : Bool}, b: Bool, eb: {b == eq(key, k) : Bool}
2366) -> {b == False{} : Bool}:
2367  match b:
2368    case True{}:
2369      h.tf({True{} == False{} : Bool}, eq(k, k), refl(k),
2370        rw(K, z => {eq(k, z) == False{} : Bool}, k, key,
2371          Equal.sym(K, key, k, sound(key, k, h.sb(True{}, eq(key, k), eb))), e))
2372    case False{}:
2373      {==}