lossimpl táctica despliega expresiones como2 + a para "hacer coincidir los árboles" que no parece simple en absoluto. Por ejemplo:

Goal forall i:Z, ((fun x => x + i) 3 = i + 3).
simpl.

Lleva a:

forall i : Z,
match i with
| 0 => 3
| Z.pos y' =>
    Z.pos
      match y' with
      | q~1 =>
          match q with
          | q0~1 => (Pos.succ q0)~1
          | q0~0 => (Pos.succ q0)~0
          | 1 => 3
          end~0
      | q~0 =>
          match q with
          | q0~1 => (Pos.succ q0)~0
          | q0~0 => q0~1
          | 1 => 2
          end~1
      | 1 => 4
      end
| Z.neg y' => Z.pos_sub 3 y'
end = i + 3

Cómo evitar tales complicaciones consimpl ¿táctica?

Este objetivo particular se puede resolver conomega, pero si es un poco más sofisticado, omega falla y tengo que recurrir a algo como:replace (2 + a) with (a + 2); simpl; replace (a + 2) with (2 + a).