val coerce_eq: #a: Type -> #b: Type -> x: a -> squash (a == b) -> y: b{y == x}
let coerce_eq (#a #b:Type) (x:a) (_:squash (a == b)) : y:b {y == x} = x
val coerce_eq: #a: Type -> #b: Type -> x: a -> squash (a == b) -> y: b{y == x}
let coerce_eq (#a: Type) (#b: Type) (x: a) (_: squash (a == b)) : y: b{y == x} =
x
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.squash Prims.eq2
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
val coerce_eq: #a: Type -> #b: Type -> x: a -> squash (a == b) -> y: b{y == x}
x: a -> _: Prims.squash (a == b) -> y: b{y == x}