val vprop_equiv_typing (#g:_) (#t0 #t1:term) (v:vprop_equiv g t0 t1)
  : GTot ((tot_typing g t0 tm_vprop -> tot_typing g t1 tm_vprop) &
          (tot_typing g t1 tm_vprop -> tot_typing g t0 tm_vprop))
let rec vprop_equiv_typing (#g:_) (#t0 #t1:term) (v:vprop_equiv g t0 t1)
  : GTot ((tot_typing g t0 tm_vprop -> tot_typing g t1 tm_vprop) &
          (tot_typing g t1 tm_vprop -> tot_typing g t0 tm_vprop))
        (decreases v)
  = match v with
    | VE_Refl _ _ -> (fun x -> x), (fun x -> x)

    | VE_Sym _ _ _ v' -> 
      let f, g = vprop_equiv_typing v' in
      g, f

    | VE_Trans g t0 t2 t1 v02 v21 ->
      let f02, f20 = vprop_equiv_typing v02 in
      let f21, f12 = vprop_equiv_typing v21 in
      (fun x -> f21 (f02 x)), 
      (fun x -> f20 (f12 x))

    | VE_Ctxt g s0 s1 s0' s1' v0 v1 ->
      let f0, f0' = vprop_equiv_typing v0 in
      let f1, f1' = vprop_equiv_typing v1 in      
      let ff (x:tot_typing g (tm_star s0 s1) tm_vprop)
        : tot_typing g (tm_star s0' s1') tm_vprop
        = let s0_typing = star_typing_inversion_l x in
          let s1_typing = star_typing_inversion_r x in
          let s0'_typing, s1'_typing = f0 s0_typing, f1 s1_typing in
          star_typing s0'_typing s1'_typing
      in
      let gg (x:tot_typing g (tm_star s0' s1') tm_vprop)
        : tot_typing g (tm_star s0 s1) tm_vprop
        = let s0'_typing = star_typing_inversion_l x in
          let s1'_typing = star_typing_inversion_r x in
          star_typing (f0' s0'_typing) (f1' s1'_typing)        
      in
      ff, gg

    | VE_Unit g t ->
      let fwd (x:tot_typing g (tm_star tm_emp t) tm_vprop)
        : tot_typing g t tm_vprop
        = let r = star_typing_inversion_r x in
          r
      in
      let bk (x:tot_typing g t tm_vprop)
        : tot_typing g (tm_star tm_emp t) tm_vprop
        = star_typing emp_typing x
      in
      fwd, bk

    | VE_Comm g t0 t1 ->
      let f t0 t1 (x:tot_typing g (tm_star t0 t1) tm_vprop)
        : tot_typing g (tm_star t1 t0) tm_vprop
        = let tt0 = star_typing_inversion_l x in
          let tt1 = star_typing_inversion_r x in
          star_typing tt1 tt0
      in
      f t0 t1, f t1 t0

    | VE_Assoc g t0 t1 t2 ->
      let fwd (x:tot_typing g (tm_star t0 (tm_star t1 t2)) tm_vprop)
        : tot_typing g (tm_star (tm_star t0 t1) t2) tm_vprop
        = let tt0 = star_typing_inversion_l x in
          let tt12 = star_typing_inversion_r x in
          let tt1 = star_typing_inversion_l tt12 in
          let tt2 = star_typing_inversion_r tt12 in
          star_typing (star_typing tt0 tt1) tt2
      in
      let bk (x : tot_typing g (tm_star (tm_star t0 t1) t2) tm_vprop)
        : tot_typing g (tm_star t0 (tm_star t1 t2)) tm_vprop
        = let tt01 = star_typing_inversion_l x in
          let tt2 = star_typing_inversion_r x in
          let tt0 = star_typing_inversion_l tt01 in
          let tt1 = star_typing_inversion_r tt01 in
          star_typing tt0 (star_typing tt1 tt2)
      in
      fwd, bk
   
    | VE_Ext g t0 t1 token ->
      let d1, d2 = vprop_eq_typing_inversion g t0 t1 token in
      (fun _ -> d2),
      (fun _ -> d1)
val vprop_equiv_typing (#g:_) (#t0 #t1:term) (v:vprop_equiv g t0 t1)
  : GTot ((tot_typing g t0 tm_vprop -> tot_typing g t1 tm_vprop) &
          (tot_typing g t1 tm_vprop -> tot_typing g t0 tm_vprop))
let rec vprop_equiv_typing (#g: _) (#t0 #t1: term) (v: vprop_equiv g t0 t1)
    : GTot
      ((tot_typing g t0 tm_vprop -> tot_typing g t1 tm_vprop) &
        (tot_typing g t1 tm_vprop -> tot_typing g t0 tm_vprop)) (decreases v) =
match v with
| VE_Refl _ _ -> (fun x -> x), (fun x -> x)
| VE_Sym _ _ _ v' ->
  let f, g = vprop_equiv_typing v' in
  g, f
| VE_Trans g t0 t2 t1 v02 v21 ->
  let f02, f20 = vprop_equiv_typing v02 in
  let f21, f12 = vprop_equiv_typing v21 in
  (fun x -> f21 (f02 x)), (fun x -> f20 (f12 x))
| VE_Ctxt g s0 s1 s0' s1' v0 v1 ->
  let f0, f0' = vprop_equiv_typing v0 in
  let f1, f1' = vprop_equiv_typing v1 in
  let ff (x: tot_typing g (tm_star s0 s1) tm_vprop) : tot_typing g (tm_star s0' s1') tm_vprop =
    let s0_typing = star_typing_inversion_l x in
    let s1_typing = star_typing_inversion_r x in
    let s0'_typing, s1'_typing = f0 s0_typing, f1 s1_typing in
    star_typing s0'_typing s1'_typing
  in
  let gg (x: tot_typing g (tm_star s0' s1') tm_vprop) : tot_typing g (tm_star s0 s1) tm_vprop =
    let s0'_typing = star_typing_inversion_l x in
    let s1'_typing = star_typing_inversion_r x in
    star_typing (f0' s0'_typing) (f1' s1'_typing)
  in
  ff, gg
| VE_Unit g t ->
  let fwd (x: tot_typing g (tm_star tm_emp t) tm_vprop) : tot_typing g t tm_vprop =
    let r = star_typing_inversion_r x in
    r
  in
  let bk (x: tot_typing g t tm_vprop) : tot_typing g (tm_star tm_emp t) tm_vprop =
    star_typing emp_typing x
  in
  fwd, bk
| VE_Comm g t0 t1 ->
  let f t0 t1 (x: tot_typing g (tm_star t0 t1) tm_vprop) : tot_typing g (tm_star t1 t0) tm_vprop =
    let tt0 = star_typing_inversion_l x in
    let tt1 = star_typing_inversion_r x in
    star_typing tt1 tt0
  in
  f t0 t1, f t1 t0
| VE_Assoc g t0 t1 t2 ->
  let fwd (x: tot_typing g (tm_star t0 (tm_star t1 t2)) tm_vprop)
      : tot_typing g (tm_star (tm_star t0 t1) t2) tm_vprop =
    let tt0 = star_typing_inversion_l x in
    let tt12 = star_typing_inversion_r x in
    let tt1 = star_typing_inversion_l tt12 in
    let tt2 = star_typing_inversion_r tt12 in
    star_typing (star_typing tt0 tt1) tt2
  in
  let bk (x: tot_typing g (tm_star (tm_star t0 t1) t2) tm_vprop)
      : tot_typing g (tm_star t0 (tm_star t1 t2)) tm_vprop =
    let tt01 = star_typing_inversion_l x in
    let tt2 = star_typing_inversion_r x in
    let tt0 = star_typing_inversion_l tt01 in
    let tt1 = star_typing_inversion_r tt01 in
    star_typing tt0 (star_typing tt1 tt2)
  in
  fwd, bk
| VE_Ext g t0 t1 token ->
  let d1, d2 = vprop_eq_typing_inversion g t0 t1 token in
  (fun _ -> d2), (fun _ -> d1)
Pulse.Typing.Combinators.fst.checked
Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.Checker.Pure.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Set.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Typing.Combinators.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.term Pulse.Typing.vprop_equiv FStar.Pervasives.Native.Mktuple2 Pulse.Typing.tot_typing Pulse.Syntax.Base.tm_vprop FStar.Pervasives.Native.tuple2 Pulse.Typing.Combinators.vprop_equiv_typing Pulse.Syntax.Base.tm_star Pulse.Typing.star_typing Pulse.Typing.star_typing_inversion_r Pulse.Typing.star_typing_inversion_l Pulse.Syntax.Base.tm_emp Pulse.Typing.emp_typing Pulse.Syntax.Base.vprop FStar.Tactics.Types.equiv_token Pulse.Typing.elab_env Pulse.Elaborate.Pure.elab_term Pulse.Typing.vprop_eq_typing_inversion
module Pulse.Typing.Combinators

module RT = FStar.Reflection.Typing
module R = FStar.Reflection.V2
module L = FStar.List.Tot
module T = FStar.Tactics.V2
module P = Pulse.Syntax.Printer

open FStar.List.Tot
open Pulse.Syntax
open Pulse.Typing
open Pulse.Checker.Pure

let rec vprop_equiv_typing (#g:_) (#t0 #t1:term) (v:vprop_equiv g t0 t1)
  : GTot ((tot_typing g t0 tm_vprop -> tot_typing g t1 tm_vprop) &
          (tot_typing g t1 tm_vprop -> tot_typing g t0 tm_vprop))
val vprop_equiv_typing (#g:_) (#t0 #t1:term) (v:vprop_equiv g t0 t1)
  : GTot ((tot_typing g t0 tm_vprop -> tot_typing g t1 tm_vprop) &
          (tot_typing g t1 tm_vprop -> tot_typing g t0 tm_vprop))
v: Pulse.Typing.vprop_equiv g t0 t1
  -> Prims.GTot
    ((_: Pulse.Typing.tot_typing g t0 Pulse.Syntax.Base.tm_vprop
          -> Pulse.Typing.tot_typing g t1 Pulse.Syntax.Base.tm_vprop) *
      (_: Pulse.Typing.tot_typing g t1 Pulse.Syntax.Base.tm_vprop
          -> Pulse.Typing.tot_typing g t0 Pulse.Syntax.Base.tm_vprop))