Based path induction is such a funny term to me, now. If you point it out it's implicitly a compliment, like "hey, based path induction! 😎"