aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4464.v
blob: f8e9405d934b8a204bc27c76bc6b8b5ce9be7703 (plain)
1
2
3
4
Goal True -> True.
Proof.
  intro H'.
  let H := H' in destruct H; try destruct H.