Search code examples
coqcoq-tactic

Coq infotheo %B is_true

I have hit the wall with a proof (Coq version 8.13.1 , using infotheo), where the context Hypothesis is as the goal, just with a "%B" attached. I understand it indicates 'is_true', but how to proceed the proof?

(unfold is_true does not get rid of "%B", rewrite H and apply H does not work).

A: finType
B: eqType
i: B
i0: A
X: A -> B
H: (X i0 == i)%B
===
(1/1)
X i0 = i

Any advice appreciated.

Solution

  • Thank you for the answers. The problem was solved by:

        move/eqP in H.
    apply H.
Qed.