Coq infotheo %B is_true

0
votes

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.

2
coqcoq-tactic
Does by apply/eqP work for you? – Anton Trunov

2 Answers

0
votes

The %B means that this is parsed in a different scope. The equality sign means something different in H and the goal. And it is == vs = btw.

You can switch off notatations to see what both terms really mean.

Likely the == is weaker than =.

0
votes

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

    move/eqP in H.
    apply H.
Qed.