while porting some files from a tutorial by assia (here)
It seems that before we could write
Definition two'' : 'I_3 := Sub 2 (refl_equal true).
but now we have to write.
Definition two'' : [subType of 'I_3] := Sub 2 (refl_equal true).
What has changed?
Did you find the reason?
Last updated: Feb 09 2023 at 02:02 UTC