# Tag Info

I eventually proved the theorem in a mechanical fashion and I want to thank j_random_hacker for pointing out a proof sketch based on induction and correcting my wrong initial formal statement. The actual (mechanical) solution did require the employment of an inductive predicate that allows the human prover to instantiate the inductive hypothesis to a set $X'$...