fix induction subgoals stored in ntac nodes; and start f-equal tactic

[stchang]

No description provided.

[stchang]

I started the most basic f-equal tactic. Now that this works, we can gradually try to make the arguments more implicit

[stchang]

re: f has no types

As I suspected, this is (partly) because this current branch is behind main. Problem described here: wilbowma#134

[stchang]

Ok I got something working for f-equal-tactic. Now you can either use it with explicit args, or no args.

(To run the example, you'll need to also pull and compile a change from Turnstile popl2020-artifact branch)