def aes_nat_eq_refl_is_some
qasim-bend-kit@0.1.0.2 · PROOF.bend:402
import qasim-bend-kit@0.1.0.2/PROOF.bend as PROOF
import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
402def aes_nat_eq_refl_is_some(+n: Nat) ->
403 {Maybe.is_some(&0, {n == n : Nat},
404 AES.aes_nat_eq_proof(n, n)) == True{} : Bool}:
405 match n:
406 case 0n: {==}
407 case 1n+p:
408 Equal.trans(Bool,
409 Maybe.is_some(&0, {1n+p == 1n+p : Nat},
410 AES.aes_nat_eq_proof(1n+p, 1n+p)),
411 Maybe.is_some(&0, {p == p : Nat},
412 AES.aes_nat_eq_proof(p, p)),
413 True{},
414 aes_nat_eq_step_status(p, p, AES.aes_nat_eq_proof(p, p)),
415 aes_nat_eq_refl_is_some(p))