This question is about the representation of relations/predicates through Idris data types. Select all statements that are true. (Note that the terms "parameter values" and "type index" are used synonymously.) It can't happen that all the types denoted by a parameterized data type contain the exact same values. A plain (i.e. non-parameterized) data type always defines a set (or nullary relation). A proof for a proposition can be given by a value or a function. A parameterized data type can denote different sets for different parameter values. A plain (i.e. non-parameterized) data type can define a subset of some other type. Different elements of a type constitute different proofs for the proposition represented by the type. A data type that has at least one constructor cannot denote an empty set and always contains elements