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.STApp.fst.checked
Pulse.Typing.FV.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked Pulse.Checker.Pure.fsti.checked Pulse.Checker.Prover.fsti.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.fsti.checked
Pulse.Checker.STApp.fst
Prims.squash Prims.op_Equals_Equals_Equals Prims.eq2
module Pulse.Checker.STApp

open Pulse.Syntax
open Pulse.Typing
open Pulse.Checker.Pure
open Pulse.Checker.Base

module T = FStar.Tactics.V2
module RT = FStar.Reflection.Typing
module FV = Pulse.Typing.FV
module RU = Pulse.RuntimeUtils
module P = Pulse.Syntax.Printer
module Prover = Pulse.Checker.Prover

let debug_log (g:env) (f:unit -> T.Tac unit) : T.Tac unit = if RU.debug_at_level (fstar_env g) "st_app" then f () else ()

let canon_comp (c:comp_st) : comp_st = 
  match readback_comp (elab_comp c) with
  | None -> c
  | Some (C_Tot _) -> c //should be impossible
  | Some c' -> c'

#push-options "--admit_smt_queries true"
let canon_comp_eq_res (g:env) (c:comp_st)
  : RT.equiv (elab_env g) (elab_term (comp_res c)) (elab_term (comp_res (canon_comp c)))
  = RT.Rel_refl _ _ _ 
#pop-options

let canonicalize_st_typing (#g:env) (#t:st_term) (#c:comp_st) (d:st_typing g t c)
  : st_typing g t (canon_comp c)
  = let c' = canon_comp c in
    let x = fresh g in
    assume ( ~(x `Set.mem` freevars (comp_post c)) /\
            ~(x `Set.mem` freevars (comp_post c')) );
    assume (st_equiv_pre c c');
    let st_eq 
      : st_equiv g c c'
      = ST_VPropEquiv g c c' x (magic ()) (magic()) (magic()) (canon_comp_eq_res g c) (magic()) (magic())
    in
    T_Equiv _ _ _ _ d st_eq
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}