val is_eq2_uvar (uvs: env) (t: term) : option (uv: var{uv `Set.mem` (freevars t)} & term)
let is_eq2_uvar (uvs:env) (t:term)
  : option (uv:var { uv `Set.mem` freevars t } & term) =
  
  match is_eq2 t with
  | None -> None
  | Some (l, r) ->
    match is_var l with
    | Some nm ->
      if Set.mem nm.nm_index (dom uvs)
      then Some (| nm.nm_index, r |)
      else None
    | None ->
      match is_var r with
      | Some nm ->
        if Set.mem nm.nm_index (dom uvs)
        then Some (| nm.nm_index, l |)
        else None
      | _ -> None
val is_eq2_uvar (uvs: env) (t: term) : option (uv: var{uv `Set.mem` (freevars t)} & term)
let is_eq2_uvar (uvs: env) (t: term) : option (uv: var{uv `Set.mem` (freevars t)} & term) =
match is_eq2 t with
| None -> None
| Some (l, r) ->
  match is_var l with
  | Some nm -> if Set.mem nm.nm_index (dom uvs) then Some (| nm.nm_index, r |) else None
  | None ->
    match is_var r with
    | Some nm -> if Set.mem nm.nm_index (dom uvs) then Some (| nm.nm_index, l |) else None
    | _ -> None
Pulse.Checker.Prover.IntroPure.fst.checked
Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.Checker.VPropEquiv.fsti.checked Pulse.Checker.Pure.fsti.checked Pulse.Checker.Prover.Util.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.Set.fsti.checked FStar.Reflection.V2.Formula.fst.checked FStar.Reflection.V2.fst.checked FStar.Range.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.Checker.Prover.IntroPure.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.term Pulse.Syntax.Pure.is_eq2 FStar.Pervasives.Native.None Prims.dtuple2 Pulse.Syntax.Base.var Prims.b2t FStar.Set.mem Pulse.Syntax.Naming.freevars Pulse.Syntax.Pure.is_var Pulse.Syntax.Base.nm Pulse.Syntax.Base.__proj__Mknm__item__nm_index Pulse.Typing.Env.dom FStar.Pervasives.Native.Some Prims.Mkdtuple2 Prims.bool FStar.Pervasives.Native.option
module Pulse.Checker.Prover.IntroPure

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

module T = FStar.Tactics.V2
module P = Pulse.Syntax.Printer
module PS = Pulse.Checker.Prover.Substs

let coerce_eq (#a #b:Type) (x:a) (_:squash (a == b)) : y:b{y == x} = x

let k_intro_pure (g:env) (p:term)
  (d:tot_typing g p tm_prop)
  (token:prop_validity g p) (frame:vprop)
  
  : T.Tac (continuation_elaborator g frame g (frame * tm_pure p)) =

  let t = wtag (Some STT_Ghost) (Tm_IntroPure {p}) in
  let c = comp_intro_pure p in
  let d : st_typing g t c = T_IntroPure g p d token in

  let x = fresh g in

  // p is well-typed in g, so it does not have x free
  assume (open_term p x == p);

  let ppname = mk_ppname_no_range "_pintrop" in
  let k : continuation_elaborator
            g (frame * tm_emp)
            (push_binding g x ppname_default tm_unit) (tm_pure p * frame) =
    continuation_elaborator_with_bind frame d (magic ()) (ppname, x) in

  let k : continuation_elaborator
            g frame
            (push_binding g x ppname_default tm_unit) (frame * tm_pure p) =
    k_elab_equiv k (magic ()) (magic ()) in

  fun post_hint r ->
  let (| t1, c1, d1 |) = r in
  let d1 : st_typing g t1 c1 = d1 in
  let empty_env = mk_env (fstar_env g) in
  assert (equal g (push_env g empty_env));
  assert (equal (push_env (push_binding g x ppname_default tm_unit) empty_env)
                (push_binding g x ppname_default tm_unit));
  let d1 : st_typing (push_binding g x ppname_default tm_unit) t1 c1 =
    st_typing_weakening
      g
      empty_env
      t1 c1 d1
      (push_binding g x ppname_default tm_unit) in

  k post_hint (| t1, c1, d1 |)

module R = FStar.Reflection.V2

// let is_eq2 (t:R.term) : option (R.term & R.term) =
//   let head, args = R.collect_app_ln t in
//   match R.inspect_ln head, args with
//   | R.Tv_FVar fv, [_; (a1, _); (a2, _)]
//   | R.Tv_UInst fv _, [_; (a1, _); (a2, _)] -> 
//     let l = R.inspect_fv fv in
//     if l = ["Pulse"; "Steel"; "Wrapper"; "eq2_prop"] ||
//        l = ["Prims"; "eq2"]
//     then Some (a1, a2)
//     else None
//   | _ -> None

let is_eq2_uvar (uvs:env) (t:term)
  : option (uv:var { uv `Set.mem` freevars t } & term) =
val is_eq2_uvar (uvs: env) (t: term) : option (uv: var{uv `Set.mem` (freevars t)} & term)
uvs: Pulse.Typing.Env.env -> t: Pulse.Syntax.Base.term
  -> FStar.Pervasives.Native.option (Prims.dtuple2 (uv:
            Pulse.Syntax.Base.var{FStar.Set.mem uv (Pulse.Syntax.Naming.freevars t)})
          (fun _ -> Pulse.Syntax.Base.term))