def equal_of_equal

qasim-bend-kit@0.1.0.2 · proof/AES_TagCompareProof.bend:27

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES

27def equal_of_equal(+a: List<&2, U32>, +b: List<&2, U32>,
28    same: {a == b : List<&2, U32>}) ->
29    {AES.bytes_equal_full_scan(a, b) == True{} : Bool}:
30    Equal.trans(Bool, AES.bytes_equal_full_scan(a, b),
31        AES.bytes_equal_full_scan(b, b), True{},
32        Equal.cong(List<&2, U32>, Bool,
33            left => AES.bytes_equal_full_scan(left, b), a, b, same),
34        equal_same(b))