val pow2_4: n:nat -> Lemma (pow2 4 = 16) [SMTPat (pow2 n)]
let pow2_4 _   = assert_norm (pow2 4 = 16)
val pow2_4: n:nat -> Lemma (pow2 4 = 16) [SMTPat (pow2 n)]
let pow2_4 _ =
assert_norm (pow2 4 = 16)
Lib.IntTypes.fst.checked
prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt128.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Int8.fsti.checked FStar.Int64.fsti.checked FStar.Int32.fsti.checked FStar.Int16.fsti.checked FStar.Int128.fsti.checked FStar.Int.Cast.Full.fst.checked FStar.Int.Cast.fst.checked FStar.Int.fsti.checked FStar.BitVector.fst.checked
Lib.IntTypes.fst
Prims.nat FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality Prims.int Prims.pow2 Prims.unit
module Lib.IntTypes

open FStar.Math.Lemmas

#push-options "--max_fuel 0 --max_ifuel 1 --z3rlimit 200"

let pow2_2 _   = assert_norm (pow2 2 = 4)
val pow2_4: n:nat -> Lemma (pow2 4 = 16) [SMTPat (pow2 n)]
n: Prims.nat -> FStar.Pervasives.Lemma (ensures Prims.pow2 4 = 16) [SMTPat (Prims.pow2 n)]