val lemma_tail_append: #a:Type -> s1:seq a{length s1 > 0} -> s2:seq a -> Lemma
  (tail (append s1 s2) == append (tail s1) s2)
let lemma_tail_append #_ s1 s2 = cut (equal (tail (append s1 s2)) (append (tail s1) s2))
val lemma_tail_append: #a:Type -> s1:seq a{length s1 > 0} -> s2:seq a -> Lemma
  (tail (append s1 s2) == append (tail s1) s2)
let lemma_tail_append #_ s1 s2 =
cut (equal (tail (append s1 s2)) (append (tail s1) s2))
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.b2t Prims.op_GreaterThan FStar.Seq.Base.length Prims.cut FStar.Seq.Base.equal FStar.Seq.Properties.tail FStar.Seq.Base.append 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

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))

let lemma_append_inj_r #_ s1 s2 t1 t2 i =
  assert (index s2 i == (index (append s1 s2) (i + length s1)));
  assert (index t2 i == (index (append t1 t2) (i + length t1)))

let lemma_append_len_disj #_ s1 s2 t1 t2 =
  cut (length (append s1 s2) == length s1 + length s2);
  cut (length (append t1 t2) == length t1 + length t2)

let lemma_append_inj #_ s1 s2 t1 t2 =
  lemma_append_len_disj s1 s2 t1 t2;
  FStar.Classical.forall_intro #(i:nat{i < length s1}) #(fun i -> index s1 i == index t1 i) (lemma_append_inj_l s1 s2 t1 t2);
  FStar.Classical.forall_intro #(i:nat{i < length s2}) #(fun i -> index s2 i == index t2 i) (lemma_append_inj_r s1 s2 t1 t2)

let lemma_head_append #_ _ _ = ()
val lemma_tail_append: #a:Type -> s1:seq a{length s1 > 0} -> s2:seq a -> Lemma
  (tail (append s1 s2) == append (tail s1) s2)
s1: FStar.Seq.Base.seq a {FStar.Seq.Base.length s1 > 0} -> s2: FStar.Seq.Base.seq a
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.Seq.Properties.tail (FStar.Seq.Base.append s1 s2) ==
      FStar.Seq.Base.append (FStar.Seq.Properties.tail s1) s2)