I am not familiar at all with `SProp`

. Is it normal to get an error message at `Qed`

:

```
Lemma test_sprop : (forall P : Prop, P) -> forall S : SProp, S.
Proof.
intros HP S.
apply HP.
Fail Qed.
```

yes

Olivier Laurent has marked this topic as resolved.

Last updated: Sep 23 2023 at 13:01 UTC