print command for a constructor of inductive predicate should print only the corresponding clause
When one uses
print C where
C is a constructor of an inductive definition, it should print
only the clause
C not the whole inductive definition.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information