val list_is_prefix_of_list (#a: Type) (l1 l2: list a) : GTot bool
val list_is_prefix_of_list (#a: Type) (l1 l2: list a) : GTot bool
let rec list_is_prefix_of_list (#a: Type) (l1: list a) (l2: list a) : GTot bool =
  match l1 with
  | [] -> true
  | hd1 :: tl1 ->
      match l2 with
      | [] -> false
      | hd2 :: tl2 -> eqb hd1 hd2 && list_is_prefix_of_list tl1 tl2
module Spec.List

open FStar.Calc
open FStar.List.Tot
open Spec.Ubool

let list_len = length
let list_contains = mem
let contains_ubool = memP
/
Spec.Ubool.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Calc.fsti.checked
Spec.List.fst
l1: Prims.list a -> l2: Prims.list a -> Prims.GTot Prims.bool
Prims.list Prims.op_AmpAmp Spec.Ubool.eqb Spec.List.list_is_prefix_of_list Prims.bool
let rec list_is_prefix_of_list (#a: Type) (l1 l2: list a) : GTot bool =
  
match l1 with
| [] -> true
| hd1 :: tl1 ->
  match l2 with
  | [] -> false
  | hd2 :: tl2 -> eqb hd1 hd2 && list_is_prefix_of_list tl1 tl2