def is_eq_refl

bend-osdev-aead@0.1.0.0 · PROOF.bend:166

import bend-osdev-aead@0.1.0.0/PROOF.bend as PROOF

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL
import bend-osdev-aead@0.1.0.0/aead.bend as Ad

166def is_eq_refl(+o: B.Octets) -> {True{} == Ad.AdTag.is_eq(o, o) : Bool}:
167  Equal.sym(Bool, B.Octets.is_eq(o, o), True{}, BL.octets_is_eq_refl(o))

Uses (6)

Used by (2)