def aes_nat_eq_is_some

qasim-bend-kit@0.1.0.2 · proof/AES_EnvelopeProof.bend:727

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

727def aes_nat_eq_is_some(+a: Nat, +b: Nat,
728    evidence: {a == b : Nat}) ->
729    {Maybe.is_some(&0, {a == b : Nat},
730        AES.aes_nat_eq_proof(a, b)) == True{} : Bool}:
731    Equal.trans(Bool,
732        Maybe.is_some(&0, {a == b : Nat}, AES.aes_nat_eq_proof(a, b)),
733        Maybe.is_some(&0, {b == b : Nat}, AES.aes_nat_eq_proof(b, b)),
734        True{},
735        Equal.cong(Nat, Bool,
736            value => Maybe.is_some(&0, {value == b : Nat},
737                AES.aes_nat_eq_proof(value, b)),
738            a, b, evidence),
739        Equal.cong(Maybe<&0, {b == b : Nat}>, Bool,
740            result => Maybe.is_some(&0, {b == b : Nat}, result),
741            AES.aes_nat_eq_proof(b, b), Some{{==}},
742            aes_nat_eq_self(b)))