Let $\Sigma$ be an alphabet and $\Sigma^*$ its Kleene closure (the set of all possible finite strings over the alphabet). Also, define the set of prefixes of $x \in \Sigma^*$ by $$ \mathrm{pre}(x) = \{x[1:i] \mid i \in \{1, \ldots, |x|\}\}, $$ where the left associative subslice operator $[m:n]$ indexes into $x$, producing the substring between the indices $m$ and $n$ of the letters in $x$.
Show by constructive induction, that for all $x, y \in \Sigma^*$, if $x \in \mathrm{pre}(y)$, then then the length of the string $|x| \leq |y|$.
An attempt
The base case is easy. The empty string $\epsilon \in \mathrm{pre}(x)$ for all $x \in \Sigma^*$, and $|\epsilon| = 0 \leq |x|$ for all strings $x \in \Sigma^*$. Therefore our base case is valid.
Assume then, that $x, y \in \Sigma^*$, so that $|x| \leq |y|$. But then what? What am I actually supposed to induce? Should I vary the lengths of both $x$ and $y$ in the induction step or what?
I guess I'm asking, what is constructive induction really, and how is it different from weak induction? In weak induction we try to show that if the claim holds for a previous element, then it holds for the following element. In strong induction we assume that the claim holds for all previous elements and deduce that it has to hold for the next element.
But what is the inductve hypothesies in the case of constructive induction?
Edit
The question also has a second part: prove $|xy| + |x| + |y|$. I guess this is where I'm actually supposed to use induction. It's just the question was presented in a way that made me think induction was necessary even in the first part.
Still, my question is still unanswered. What is the inductive hypothesis (in general) when dealing with constructive induction?