proposition: Lemma eqnP: forall x y, reflect (x = y) (eqn x y).
proof: Proof. induction x; destruct y; try (constructor; done). change (eqn (S x) (S y)) with (eqn x y). case IHx; constructor; congruence. Qed.
imports: Bool Arith ZArith String ClassicalDescription FunctionalExtensionality