val apply_squash_or_lem : d:nat -> term -> Tac unit
let rec apply_squash_or_lem d t =
    (* Before anything, try a vanilla apply and apply_lemma *)
    try apply t with | _ ->
    try apply (`FStar.Squash.return_squash); apply t with | _ ->
    try apply_lemma t with | _ ->

    // Fuel cutoff, just in case.
    if d <= 0 then fail "mapply: out of fuel" else begin

    let ty = tc (cur_env ()) t in
    let tys, c = collect_arr ty in
    match inspect_comp c with
    | C_Lemma pre post _ ->
       begin
       let post = `((`#post) ()) in (* unthunk *)
       let post = norm_term [] post in
       (* Is the lemma an implication? We can try to intro *)
       match term_as_formula' post with
       | Implies p q ->
           apply_lemma (`push1);
           apply_squash_or_lem (d-1) t

       | _ ->
           fail "mapply: can't apply (1)"
       end
    | C_Total rt ->
       begin match unsquash_term rt with
       (* If the function returns a squash, just apply it, since our goals are squashed *)
       | Some rt ->
        // DUPLICATED, refactor!
         begin
         let rt = norm_term [] rt in
         (* Is the lemma an implication? We can try to intro *)
         match term_as_formula' rt with
         | Implies p q ->
             apply_lemma (`push1);
             apply_squash_or_lem (d-1) t

         | _ ->
             fail "mapply: can't apply (1)"
         end

       (* If not, we can try to introduce the squash ourselves first *)
       | None ->
        // DUPLICATED, refactor!
         begin
         let rt = norm_term [] rt in
         (* Is the lemma an implication? We can try to intro *)
         match term_as_formula' rt with
         | Implies p q ->
             apply_lemma (`push1);
             apply_squash_or_lem (d-1) t

         | _ ->
             apply (`FStar.Squash.return_squash);
             apply t
         end
       end
    | _ -> fail "mapply: can't apply (2)"
    end
val apply_squash_or_lem : d:nat -> term -> Tac unit
let rec apply_squash_or_lem d t =
try apply t
with
| _ ->
  try
    (apply (`FStar.Squash.return_squash);
      apply t)
  with
  | _ ->
    try apply_lemma t
    with
    | _ ->
      if d <= 0
      then fail "mapply: out of fuel"
      else
        let ty = tc (cur_env ()) t in
        let tys, c = collect_arr ty in
        match inspect_comp c with
        | C_Lemma pre post _ ->
          let post = `((`#post) ()) in
          let post = norm_term [] post in
          (match term_as_formula' post with
            | Implies p q ->
              apply_lemma (`push1);
              apply_squash_or_lem (d - 1) t
            | _ -> fail "mapply: can't apply (1)")
        | C_Total rt ->
          (match unsquash_term rt with
            | Some rt ->
              let rt = norm_term [] rt in
              (match term_as_formula' rt with
                | Implies p q ->
                  apply_lemma (`push1);
                  apply_squash_or_lem (d - 1) t
                | _ -> fail "mapply: can't apply (1)")
            | None ->
              let rt = norm_term [] rt in
              match term_as_formula' rt with
              | Implies p q ->
                apply_lemma (`push1);
                apply_squash_or_lem (d - 1) t
              | _ ->
                apply (`FStar.Squash.return_squash);
                apply t)
        | _ -> fail "mapply: can't apply (2)"
FStar.Tactics.MApply.fst.checked
prims.fst.checked FStar.Tactics.V2.SyntaxHelpers.fst.checked FStar.Tactics.V2.SyntaxCoercions.fst.checked FStar.Tactics.V2.Derived.fst.checked FStar.Tactics.V2.Builtins.fsti.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Tactics.NamedView.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Squash.fsti.checked FStar.Reflection.V2.Formula.fst.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.fsti.checked
FStar.Tactics.MApply.fst
Prims.nat FStar.Tactics.NamedView.term FStar.Tactics.V2.Derived.try_with Prims.unit FStar.Tactics.V2.Derived.apply Prims.exn FStar.Tactics.V2.Derived.apply_lemma Prims.op_LessThanOrEqual FStar.Tactics.V2.Derived.fail Prims.bool Prims.list FStar.Reflection.Types.typ FStar.Tactics.NamedView.comp FStar.Tactics.NamedView.inspect_comp FStar.Reflection.Types.term FStar.Tactics.MApply.apply_squash_or_lem Prims.op_Subtraction FStar.Reflection.V2.Formula.formula FStar.Reflection.V2.Formula.term_as_formula' FStar.Tactics.V2.Derived.norm_term Prims.Nil FStar.Pervasives.norm_step FStar.Reflection.V2.Derived.unsquash_term FStar.Reflection.V2.Data.comp_view FStar.Pervasives.Native.tuple2 FStar.Tactics.V2.SyntaxHelpers.collect_arr FStar.Tactics.V2.Builtins.tc FStar.Reflection.Types.env FStar.Tactics.V2.Derived.cur_env
module FStar.Tactics.MApply

open FStar.Reflection.V2
open FStar.Reflection.V2.Formula

open FStar.Tactics.Effect
open FStar.Tactics.V2.Builtins
open FStar.Tactics.NamedView
open FStar.Tactics.V2.SyntaxHelpers
open FStar.Tactics.V2.Derived
open FStar.Tactics.V2.SyntaxCoercions

open FStar.Tactics.Typeclasses

private val push1 : (#p:Type) -> (#q:Type) ->
                        squash (p ==> q) ->
                        squash p ->
                        squash q
private let push1 #p #q f u = ()

private val push1' : (#p:Type) -> (#q:Type) ->
                         (p ==> q) ->
                         squash p ->
                         squash q
private let push1' #p #q f u = ()

(*
 * Some easier applying, which should prevent frustration
 * (or cause more when it doesn't do what you wanted to)
 *)
val apply_squash_or_lem : d:nat -> term -> Tac unit
let rec apply_squash_or_lem d t =
val apply_squash_or_lem : d:nat -> term -> Tac unit
d: Prims.nat -> t: FStar.Tactics.NamedView.term -> FStar.Tactics.Effect.Tac Prims.unit