test-suite/success/clear.v


1
2
3
4
5
6

Goal forall x:nat, (forall x, x=0 -> True)->True.
  intros; eapply H.
  instantiate (1:=(fun y => _) (S x)).
  simpl.
  clear x || trivial.
Qed.