I am not familiar at all with
SProp. Is it normal to get an error message at
Lemma test_sprop : (forall P : Prop, P) -> forall S : SProp, S. Proof. intros HP S. apply HP. Fail Qed.
Olivier Laurent has marked this topic as resolved.
Last updated: Sep 23 2023 at 13:01 UTC