val lemma_append_inj_l: #a:Type -> s1:seq a -> s2:seq a -> t1:seq a -> t2:seq a{length s1 = length t1 /\ equal (append s1 s2) (append t1 t2)} -> i:nat{i < length s1}
  -> Lemma (index s1 i == index t1 i)
let lemma_append_inj_l #_ s1 s2 t1 t2 i =
  assert (index s1 i == (index (append s1 s2) i));
  assert (index t1 i == (index (append t1 t2) i))
val lemma_append_inj_l: #a:Type -> s1:seq a -> s2:seq a -> t1:seq a -> t2:seq a{length s1 = length t1 /\ equal (append s1 s2) (append t1 t2)} -> i:nat{i < length s1}
  -> Lemma (index s1 i == index t1 i)
let lemma_append_inj_l #_ s1 s2 t1 t2 i =
assert (index s1 i == (index (append s1 s2) i));
assert (index t1 i == (index (append t1 t2) i))
FStar.Seq.Properties.fst.checked
prims.fst.checked FStar.Squash.fsti.checked FStar.Seq.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Properties.fst.checked FStar.List.Tot.Base.fst.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
FStar.Seq.Properties.fst
FStar.Seq.Base.seq Prims.l_and Prims.b2t Prims.op_Equality Prims.nat FStar.Seq.Base.length FStar.Seq.Base.equal FStar.Seq.Base.append Prims.op_LessThan Prims._assert Prims.eq2 FStar.Seq.Base.index Prims.unit
(*
   Copyright 2008-2014 Nikhil Swamy and Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module FStar.Seq.Properties

open FStar.Seq.Base
module Seq = FStar.Seq.Base
val lemma_append_inj_l: #a:Type -> s1:seq a -> s2:seq a -> t1:seq a -> t2:seq a{length s1 = length t1 /\ equal (append s1 s2) (append t1 t2)} -> i:nat{i < length s1}
  -> Lemma (index s1 i == index t1 i)

    s1: FStar.Seq.Base.seq a ->
    s2: FStar.Seq.Base.seq a ->
    t1: FStar.Seq.Base.seq a ->
    t2:
      FStar.Seq.Base.seq a
        { FStar.Seq.Base.length s1 = FStar.Seq.Base.length t1 /\
          FStar.Seq.Base.equal (FStar.Seq.Base.append s1 s2) (FStar.Seq.Base.append t1 t2) } ->
    i: Prims.nat{i < FStar.Seq.Base.length s1}
  -> FStar.Pervasives.Lemma (ensures FStar.Seq.Base.index s1 i == FStar.Seq.Base.index t1 i)