val lemma_upd_eq (r:reg) (v:t_reg r) (m:t) : Lemma
  (requires True)
  (ensures sel r (upd r v m) == v)
  [SMTPat (sel r (upd r v m))]
let lemma_upd_eq r v m =
  assert_norm (sel r (upd r v m) == v)
val lemma_upd_eq (r:reg) (v:t_reg r) (m:t) : Lemma
  (requires True)
  (ensures sel r (upd r v m) == v)
  [SMTPat (sel r (upd r v m))]
let lemma_upd_eq r v m =
assert_norm (sel r (upd r v m) == v)
Vale.X64.Regs.fst.checked
Vale.X64.Machine_s.fst.checked Vale.Lib.Map16.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.X64.Regs.fst
Vale.X64.Machine_s.reg Vale.X64.Machine_s.t_reg Vale.X64.Regs.t FStar.Pervasives.assert_norm Prims.eq2 Vale.X64.Regs.sel Vale.X64.Regs.upd Prims.unit
module Vale.X64.Regs
open FStar.Mul
open Vale.X64.Machine_s

let of_fun m =
  reveal_opaque (`%sel) sel;
//  FStar.FunctionalExtensionality.on_dom reg m
  let m0_3 = ((m (Reg 0 0), m (Reg 0 1)), (m (Reg 0 2), m (Reg 0 3))) in
  let m4_7 = ((m (Reg 0 4), m (Reg 0 5)), (m (Reg 0 6), m (Reg 0 7))) in
  let m8_11 = ((m (Reg 0 8), m (Reg 0 9)), (m (Reg 0 10), m (Reg 0 11))) in
  let m12_15 = ((m (Reg 0 12), m (Reg 0 13)), (m (Reg 0 14), m (Reg 0 15))) in
  let m0 = ((m0_3, m4_7), (m8_11, m12_15)) in
  let m0_3 = ((m (Reg 1 0), m (Reg 1 1)), (m (Reg 1 2), m (Reg 1 3))) in
  let m4_7 = ((m (Reg 1 4), m (Reg 1 5)), (m (Reg 1 6), m (Reg 1 7))) in
  let m8_11 = ((m (Reg 1 8), m (Reg 1 9)), (m (Reg 1 10), m (Reg 1 11))) in
  let m12_15 = ((m (Reg 1 12), m (Reg 1 13)), (m (Reg 1 14), m (Reg 1 15))) in
  let m1 = ((m0_3, m4_7), (m8_11, m12_15)) in
  (m0, m1)
(*
  let m0_3 = ((m rRax, m rRbx), (m rRcx, m rRdx)) in
  let m4_7 = ((m rRsi, m rRdi), (m rRbp, m rRsp)) in
  let m8_11 = ((m rR8, m rR9), (m rR10, m rR11)) in
  let m12_15 = ((m rR12, m rR13), (m rR14, m rR15)) in
  let m' = ((m0_3, m4_7), (m8_11, m12_15)) in
  assert_norm (m rRax == sel rRax m');
  assert_norm (m rRbx == sel rRbx m');
  assert_norm (m rRcx == sel rRcx m');
  assert_norm (m rRdx == sel rRdx m');
  assert_norm (m rRsi == sel rRsi m');
  assert_norm (m rRdi == sel rRdi m');
  assert_norm (m rRbp == sel rRbp m');
  assert_norm (m rRsp == sel rRsp m');
  assert_norm (m rR8  == sel rR8  m');
  assert_norm (m rR9  == sel rR9  m');
  assert_norm (m rR10 == sel rR10 m');
  assert_norm (m rR11 == sel rR11 m');
  assert_norm (m rR12 == sel rR12 m');
  assert_norm (m rR13 == sel rR13 m');
  assert_norm (m rR14 == sel rR14 m');
  assert_norm (m rR15 == sel rR15 m');
  m'
*)
val lemma_upd_eq (r:reg) (v:t_reg r) (m:t) : Lemma
  (requires True)
  (ensures sel r (upd r v m) == v)
  [SMTPat (sel r (upd r v m))]
r: Vale.X64.Machine_s.reg -> v: Vale.X64.Machine_s.t_reg r -> m: Vale.X64.Regs.t
  -> FStar.Pervasives.Lemma (ensures Vale.X64.Regs.sel r (Vale.X64.Regs.upd r v m) == v)
      [SMTPat (Vale.X64.Regs.sel r (Vale.X64.Regs.upd r v m))]