val list_append_index2: #a:Type -> x:list a -> y:list a -> i:nat{FL.length x <= i /\ i < FL.length x + FL.length y} ->
  Lemma (ensures (FL.(index (x @ y)) i == FL.index y (i - FL.length x))) (decreases (FL.length x))
let rec list_append_index2 #a x y i =
  match x with
  | [] -> ()
  | hd::tl -> list_append_index2 tl y (i - 1)
val list_append_index2: #a:Type -> x:list a -> y:list a -> i:nat{FL.length x <= i /\ i < FL.length x + FL.length y} ->
  Lemma (ensures (FL.(index (x @ y)) i == FL.index y (i - FL.length x))) (decreases (FL.length x))
let rec list_append_index2 #a x y i =
match x with
| [] -> ()
| hd :: tl -> list_append_index2 tl y (i - 1)
Hacl.Spec.PrecompBaseTable.fst.checked
Spec.Exponentiation.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.Definition.fsti.checked Hacl.Impl.Exponentiation.Definitions.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Hacl.Spec.PrecompBaseTable.fst
Prims.list Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.List.Tot.Base.length Prims.op_LessThan Prims.op_Addition Hacl.Spec.PrecompBaseTable.list_append_index2 Prims.op_Subtraction Prims.unit
module Hacl.Spec.PrecompBaseTable

open FStar.Mul
open Lib.IntTypes

module FL = FStar.List.Tot
module LSeq = Lib.Sequence

module LE = Lib.Exponentiation.Definition
module SE = Spec.Exponentiation
module BE = Hacl.Impl.Exponentiation.Definitions

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

#push-options "--fuel 2"
val list_append_index1: #a:Type -> x:list a -> y:list a -> i:nat{i < FL.length x} ->
  Lemma (ensures (FL.(index (x @ y)) i == FL.index x i)) (decreases (FL.length x))

let rec list_append_index1 #a x y i =
  match x with
  | [] -> ()
  | hd::tl -> if i = 0 then () else list_append_index1 tl y (i - 1)


val list_append_index2: #a:Type -> x:list a -> y:list a -> i:nat{FL.length x <= i /\ i < FL.length x + FL.length y} ->
  Lemma (ensures (FL.(index (x @ y)) i == FL.index y (i - FL.length x))) (decreases (FL.length x))
val list_append_index2: #a:Type -> x:list a -> y:list a -> i:nat{FL.length x <= i /\ i < FL.length x + FL.length y} ->
  Lemma (ensures (FL.(index (x @ y)) i == FL.index y (i - FL.length x))) (decreases (FL.length x))

    x: Prims.list a ->
    y: Prims.list a ->
    i:
      Prims.nat
        { FStar.List.Tot.Base.length x <= i /\
          i < FStar.List.Tot.Base.length x + FStar.List.Tot.Base.length y }
  -> FStar.Pervasives.Lemma
      (ensures
        FStar.List.Tot.Base.index (x @ y) i ==
        FStar.List.Tot.Base.index y (i - FStar.List.Tot.Base.length x))
      (decreases FStar.List.Tot.Base.length x)