Goal True -> True.
Proof.
  intro H'.
  let H := H' in destruct H; try destruct H.