def AP.con_cong

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

import Base

817def AP.con_cong(-T: Data, -h: T, -x: List<&2, T>, -y: List<&2, T>, e: {x == y : List<&2, T>}) -> {Con{h, x} == Con{h, y} : List<&2, T>}:
818  %e : {Con{h, x} == Con{h, _} : List<&2, T>}
819  {==}