def DoubleGoal

stelliferous@0.0.2.0 · proofs/u32_shift.bend:82

import Base

82def DoubleGoal(+w: Word(32n)) -> Type:
83  {U32.is_lt(U32{w},2147483648) == True{} : Bool} -> {Word.to_nat(32n,Word.shl(32n,w)) == Nat.double(Word.to_nat(32n,w)) : Nat}