val no_repeats (l: list var) : Type0
let rec no_repeats (l:list var) : Type0 =
  match l with
  | [] -> True
  | x::tl -> (~ (L.memP x tl)) /\ no_repeats tl
val no_repeats (l: list var) : Type0
let rec no_repeats (l: list var) : Type0 =
match l with
| [] -> True
| x :: tl -> (~(L.memP x tl)) /\ no_repeats tl
Pulse.Checker.Prover.Substs.fst.checked
Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.Env.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.fst.checked prims.fst.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked FStar.IndefiniteDescription.fsti.checked
Pulse.Checker.Prover.Substs.fst
Prims.list Pulse.Syntax.Base.var Prims.l_True Prims.l_and Prims.l_not FStar.List.Tot.Base.memP Pulse.Checker.Prover.Substs.no_repeats
module Pulse.Checker.Prover.Substs

open FStar.List.Tot

open Pulse.Syntax
open Pulse.Typing.Env
open Pulse.Typing

module L = FStar.List.Tot
module Env = Pulse.Typing.Env
module Metatheory = Pulse.Typing.Metatheory

let coerce_eq (#a #b:Type) (x:a) (_:squash (a == b)) : y:b {y == x} = x
val no_repeats (l: list var) : Type0
l: Prims.list Pulse.Syntax.Base.var -> Type0