aqjune

open tactic

private constant mk_eq (sz:size) (x y:bitvector sz): x = y
constant smt_eq {sz:size}: sbitvec sz → sbitvec sz → Prop

theorem eq_add2 (sz:size): ∀ (x y: bitvector sz),
    smt_eq (sbitvec.add (sbitvec.of_bv x) (sbitvec.of_bv y))
           (sbitvec.of_bv (bitvector.add x y)) :=
by do
  x ← intro `x,