Generate all projectors/method via the tactic

```fstar
unfold
let maybe_ghost (b:bool) (post : unit -> prop) =
if b
then unit -> squash (post ())
else unit -> squash (post ())

noeq
type r (p:Type) = {
ghost : bool;
pred : p -> prop;
( ! ) : y:p -> maybe_ghost ghost (fun _ -> pred y);
}
```

Error:
```
* Error 19 at LimitationOfProjectors.fst(13,5-13,6):
- Subtyping check failed; expected type y: p
-> maybe_ghost (Mkr?.ghost (Mkr ghost pred op_Bang))
(fun _ -> Mkr?.pred (Mkr ghost pred op_Bang) y); got type y: p -> maybe_ghost ghost (fun _ -> pred y)
- The SMT solver could not prove the query. Use --query_stats for more
details.
- See also LimitationOfProjectors.fst(13,18-13,53)
```

Query (from .smt2):
```
; Encoding query formula : forall (p: Type)
; (projectee: LimitationOfProjectors.r p)
; (b: Prims.bool)
; (b: (_: p -> Prims.prop))
; (b:
; (y: p
; -> ((match b with
; | true -> _: Prims.unit -> Prims.squash (b y)
; | _ -> _: Prims.unit -> Prims.squash (b y))
; <:
; Type)))
; (_: _: Prims.unit{projectee == LimitationOfProjectors.Mkr b b b})
; (y: p).
; (*Subtyping check failed; expected type y: p
; -> maybe_ghost (Mkr?.ghost (Mkr ghost pred op_Bang))
; (fun _ -> Mkr?.pred (Mkr ghost pred op_Bang) y); got type y: p -> maybe_ghost ghost (fun _ -> pred y)*)
; (match b with
; | true -> _: Prims.unit -> Prims.squash (b y)
; | _ -> _: Prims.unit -> Prims.squash (b y)) ==
; (match Mkr?.ghost (LimitationOfProjectors.Mkr b b b) with
; | true -> _: Prims.unit -> Prims.squash (Mkr?.pred (LimitationOfProjectors.Mkr b b b) y)
; | _ -> _: Prims.unit -> Prims.squash (Mkr?.pred (LimitationOfProjectors.Mkr b b b) y))
```

I think this fails due to a combination of the dependency and use of `pred` under a binder in `(!)`'s type, so https://github.com/FStarLang/FStar/issues/1948 applies. It actually works if we just unfold the projectors for `ghost` and `pred` before checking `(!)`.

While that unfolding may work, with @nikswamy we're thinking using the tactic from [https://github.com/FStarLang/FStar/issues/1355#issuecomment-723318882](https://github.com/FStarLang/FStar/issues/1355#issuecomment-723318882) would be better overall. Trying...