The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

Hi,

In the proof state below:

1 subgoals

r' : re

r'' : re

a' : f_automata

a'' : f_automata

H : re_fa_equiv_concept r' a' /\ re_fa_equiv_concept r'' a''

s : string

H0 : fa_belongs_p s (fa_uni a' a'')

______________________________________(1/1)

re_matches r' (Some s) \/ re_matches r'' (Some s)

where:

Lemma fa_uni_str: 

      forall s: string, 

      forall a1 a2: f_automata, 

      (fa_belongs_p s a1) \/ (fa_belongs_p s a2) -> (fa_belongs_p s (fa_uni a1 a2)).

I want to add to the context the new hypothesis H1: (fa_belongs_p s a') \/ (fa_belongs_p s a'') (assumptions of the lemma above).

However, Coq does not accept the tactic "apply (fa_uni_str s a' a'') in H0" ("Unable to unify"). What is wrong? How can this be done?

Thank you.

Marcus.