Tactic blocks are desugared

For example `map_equal_lemma` in `FStar.FiniteMap.Base` produces prompt/expected_response fields like this:
```fstar
let map_equal_lemma () : Lemma (map_equal_fact u#b)
= FStar.Tactics.Effect.assert_by_tactic (map_equal_fact u#b)
(fun _ ->
();
(T.norm [delta_only [`%map_equal_fact]];
let _ = T.forall_intro () in
let _ = T.forall_intro () in
let _ = T.forall_intro () in
let _ = T.forall_intro () in
T.split ();
T.smt ();
T.smt ()))
```

Start by examining the `map_equal_lemma` example in `FStar.FiniteMap.Base` and the generated `prompt` and `expected_response` fields shown in the issue. Clarify the intended desugaring behavior and define a reproducible expected result before locating an implementation entry point or test.

Written by the indexing model from the issue text.