§ Type formers need not be injective
abbrev Powerset (X: Type) := X -> Prop -- the powerset of a type is the collection of all subsets.
- This shows that we can create type formers which are not injective.
- This means that inductives are indeed special, for us to be able to have that, eg,
cons a as = cons b bs implies that
a = b /\ b = bs.