DEBSOURCES
Skip Quicknav
sources / coq / 8.20.1%2Bdfsg-1 / test-suite / ssr / caseeqltac.v
123456789
Require Import ssreflect. Goal (1 + 2 = 3). Proof. let E := fresh "F" in move E: (2 in LHS) => n. rewrite F. by []. Qed.