blob: 6cd0434926b77b048454a05c54d5db4de541edc0 (
plain)
1
2
3
4
5
6
7
8
|
(* Check that constraints on definitions are preserved by discharging *)
Section A.
Definition Type2 := Type.
Definition Type1 : Type2 := Type.
End A.
Definition Inconsistency : Type1 := Type2.
|