Module proof
indexing
Length marker for range known to not be empty.
Length marker for unknown length.
Represents the combination of two proofs P and Q by a new type Sum.
P
Q
Sum