The Coq mailing list

["Ly Kim Quyen (Gwenhael)" <lykimq AT gmail.com>]

Dear list, 

Here is the order of my section. 

Section S.

 Variable nat_of_string : string -> nat.

  Section color.

   ....
    Notation aterm := (ATerm.term Sig).
    Notation arule := (ATrs.rule Sig). 
    Notation arules := (ATrs.rules Sig).
    Notation abrule := (ATrs.brule).
  ... 

    Section order.

     ....
   
    Definition bsucc_ge := brel succ_ge_dec.
    Lemma bsucc_ge_sub : rel bsucc_ge << succ_ge.
     ....
    End order.

 Definition redPair_interpretation ...

 Lemma redPair_interpretation_ok ...

 End color.
 ...

End S.

Here is my problem.

When I am proving the Lemma redPair_interpretation_ok,  at this goal, it gives me the different context:

  nat_of_string : string -> nat
  arity : symbol -> nat
  R : arules
  d : domain
  d0 : degree
  is : list interpret

  R' : arules
  bsucc_ge : aterm -> aterm -> bool
  bsucc_gt : aterm -> aterm -> bool
  H : forallb (abrule bsucc_ge) R = true
  H0 : Ok (filter (abrule (neg bsucc_gt)) R) = Ok R'
  H1 : WF (red R')

  Rge := filter (abrule (neg bsucc_gt)) R : list arule
  Rgt := removes eq_rule_dec Rge R : list arule
  l : aterm
  r : aterm
  h : In {| lhs := l; rhs := r |} R
  ============================
   rp_succ_eq rp l r

When I apply the lemma: apply bsucc_ge_sub. The goal is:  rel color.bsucc_ge l r , where rp_succ_eq (Constant CoLoR.Term.WithArity.ARelation.rp_succ_eq)

I go further and I meet the hypothesis H with bsucc_ge. I cannot use the tactic: apply H. to be able to using the hypothesis h to finish my goal. 

  nat_of_string : string -> nat
  arity : symbol -> nat
  R : arules
  d : domain
  d0 : degree
  is : list interpret

  R' : arules
  bsucc_ge : aterm -> aterm -> bool
  bsucc_gt : aterm -> aterm -> bool
  H : forall x : arule, In x R -> abrule bsucc_ge x = true
  H0 : Ok (filter (abrule (neg bsucc_gt)) R) = Ok R'

  H1 : WF (red R')
  Rge := filter (abrule (neg bsucc_gt)) R : list arule
  Rgt := removes eq_rule_dec Rge R : list arule
  l : aterm
  r : aterm
  h : In {| lhs := l; rhs := r |} R
  ============================

   abrule color.bsucc_ge {| lhs := l; rhs := r |} = true


How I can use the hypothesis H?

I am sorry if my code given is not enough information. 

Thank you very much,

Gwen