I am formalizing the untyped lambda calculus, and as part of sanity-checking my work as I go I have a number of test cases I like to work with.

```
Goal beta_reduces_to (id $ id) id.
Proof.
constructor.
Qed.
Goal beta_reduces_to infinite_loop infinite_loop.
Proof.
constructor.
Qed.
Goal beta_reduces_to fork_bomb (fork_bomb $ fork_bomb).
Proof.
constructor.
Qed.
```

It occured to me that I could fold these together using `Forall`

from the standard library:

```
Goal Forall (fun (t: prod Term Term) => beta_reduces_to (fst t) (snd t)) [
((id $ id), id);
(infinite_loop, infinite_loop);
(fork_bomb, (fork_bomb $ fork_bomb))
].
Proof.
apply Forall_forall.
intros.
repeat (induction H; [subst; simpl; constructor | idtac]).
inversion H.
Qed.
```

Is this the â€śmorally correctâ€ť approach to this? I would have preferred to use reflection to do the iteration within Gallina instead of using `repeat`

but Iâ€™m not sure there is a quick and easy way to do that.