Hola Camilo.
Si, destruct está habilitada. AL usarla podés luego usar apply sobre h1 y verás que se generan dos obligaciones de prueba triviales.
Otra opción es usar (de lo visto en la clase): elim h2. Luego de hacer intros estás en la situación descrita arriba.
Saludos, Carlos