Suppose I have something like

```
Parameter X Y Z: Set.
Axiom foo : X -> Y -> Z.
Axiom x : X.
Axiom y : Y.
Lemma test : Z.
Proof.
apply/foo/y/x.
Qed.
```

Why do chained `apply`

views work on the last generated goal rather than the top one, i.e. the proof above works but `apply/foo/x/y`

doesn't?

Last updated: Feb 08 2023 at 07:02 UTC