= と == の言い換え

eqP
     : reflect (?x = ?y) (?x == ?y)

を move/ して使う.

1 subgoal
  
  n, m : nat
  ============================
  n = m -> n == m

ex <   move/eqP.
1 subgoal
  
  n, m : nat
  ============================
  n == m -> n == m

1 subgoal
  
  n, m : nat
  ============================
  n == m -> n = m

ex <   move/eqP.
1 subgoal
  
  n, m : nat
  ============================
  n = m -> n = m