move_after.v « ssrtest « mathcomp - coq-mathcomp - Library of mathematical components formalized in Coq

about summary refs log tree commit diff

path: root/mathcomp/ssrtest/move_after.v

blob: d62926d541288b4ced7d90166728eff503bbf187 (plain)

Require Import mathcomp.ssreflect.ssreflect.


Goal True -> True -> True.
move=> H1 H2.
move H1 after H2.
Admitted.