1 2 3 4 5 6
From Coq Require Import ssreflect. Lemma normalizeP (p : tt = tt) : p = p. Proof. Fail move: {2} tt p. Abort.