@jer_gib@functional.cafe That's the essence of the proof, yes, but one is still relying here on induction in a way that we haven't taught them yet at this point. Which is a self-inflicted problem, I agree ;-)