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.IntroExists.fst.checked
Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Checker.VPropEquiv.fsti.checked Pulse.Checker.Prover.Substs.fsti.checked Pulse.Checker.Prover.Base.fsti.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.Checker.Prover.IntroExists.fst
Prims.squash Prims.eq2
module Pulse.Checker.Prover.IntroExists

open Pulse.Syntax
open Pulse.Typing
open Pulse.Typing.Combinators
open Pulse.Typing.Metatheory
open Pulse.Checker.VPropEquiv
open Pulse.Checker.Prover.Base
open Pulse.Checker.Base

module T = FStar.Tactics.V2
module PS = Pulse.Checker.Prover.Substs
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}