I have a question about proof by induction in the domain of session types. Let's assume we have the following lemma:
$$ \text{Let}~ \Gamma \vdash P : T. ~~\text{If } P = \mu X. Q ~~\text{then}~~ \Gamma, X:T \vdash Q: T $$
Now, I want to prove it by induction. I am quite familiar with the concept of "proof by induction" in maths but when I try to apply it to the area of $\pi$-calculus or session types, I don't quite understand how to do it. For example, in the above lemma:
- What would be the base case?
- What is the induction hypothesis?