autoclean.v « ssr « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/ssr/autoclean.v

blob: db80a622595c79228f76696e78c6e3b96e36d5a4 (plain)

Require Import ssreflect.

Lemma view_disappears A B (AB : A -> B) : A -> False.
Proof. move=> {}/(AB). have := AB. Abort.