test-suite/bugs/closed/5065.v


1
2
3
4
5
6

Inductive foo := C1 : bar -> foo with bar := C2 : foo -> bar.

Lemma L1 : foo -> True with L2 : bar -> True.
intros; clear L1 L2; abstract (exact I).
intros; exact I.
Qed.