val unsquash_equality (t: term) : Tac (option (term & term))
let unsquash_equality (t:term) : Tac (option (term & term)) =
  begin match term_as_formula t with
  | Comp (Eq _) l r -> Some (l, r)
  | _ -> None
  end
val unsquash_equality (t: term) : Tac (option (term & term))
let unsquash_equality (t: term) : Tac (option (term & term)) =
match term_as_formula t with
| Comp (Eq _) l r -> Some (l, r)
| _ -> None
FStar.InteractiveHelpers.PostProcess.fst.checked
prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.InteractiveHelpers.Propositions.fst.checked FStar.InteractiveHelpers.Output.fst.checked FStar.InteractiveHelpers.ExploreTerm.fst.checked FStar.InteractiveHelpers.Effectful.fst.checked FStar.InteractiveHelpers.Base.fst.checked
FStar.InteractiveHelpers.PostProcess.fst
FStar.Reflection.Types.term FStar.Pervasives.Native.option FStar.Reflection.Types.typ FStar.Pervasives.Native.Some FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.Mktuple2 FStar.Reflection.V1.Formula.formula FStar.Pervasives.Native.None FStar.Reflection.V1.Formula.term_as_formula
module FStar.InteractiveHelpers.PostProcess

open FStar.List
open FStar.Tactics
open FStar.Mul
open FStar.InteractiveHelpers.Base
open FStar.InteractiveHelpers.ExploreTerm
open FStar.InteractiveHelpers.Propositions
open FStar.InteractiveHelpers.Effectful
open FStar.InteractiveHelpers.Output

let term_eq = FStar.Tactics.term_eq_old

/// The high-level post-processing tactics, used to retrieve some specific
/// information from the context and generate output which can be exploited
/// on the IDE side.

#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" 

(*** General utilities *)
/// We declare some identifiers that we will use to guide the meta processing
assume type meta_info
assume val focus_on_term : meta_info

let end_proof () =
  tadmit_t (`())
val unsquash_equality (t: term) : Tac (option (term & term))
t: FStar.Reflection.Types.term
  -> FStar.Tactics.Effect.Tac
    (FStar.Pervasives.Native.option (FStar.Reflection.Types.term * FStar.Reflection.Types.term))