test-suite/bugs/closed/6910.v


1
2
3
4
5

From Coq Require Import ssreflect ssrfun.

(* We should be able to use Some_inj as a view: *)
Lemma foo (x y : nat) : Some x = Some y -> x = y.
Proof. by move/Some_inj. Qed.