[MetaPRL Users] Term extraction problem

[Wojtek Moczydlowski]

   Thanks for the answer to the previous email. Here's even simpler question.
The relevant fragment of my theory file are:

prim axiomVar {| elim |} 'H :
     sequent { <H>; v : 't; <J['v]> >- 't } = 'v

prim lamAbs {| intro |} :
     ('m['v] : sequent { <H>; v : 't >- 't1}) -->
      sequent { <H> >- arrow{'t;'t1}} = lambda{'t; v.'m['v]}

interactive i 't1 :
      sequent { >- arrow {'t1;'t1}}

So I'm trying to prove t1 -> t1. Obviously I start by applying lamAbs, and
then I want to apply axiomVar. However, no matter what number I try to use
it with, it doesn't work:

# ls ""

# <*>
....main....
. arrow{t1; t1}

BY lamAbs

1. [#]
    ....main....
       t1 . t1
       () : unit
# refine axiomVar 0
       Refine error:
           Rewrite_match_redex.match_redex_sequent_hyps:
                  not enough hypotheses when matching hypothesis number 1
# refine axiomVar 1
                  Refine error:
                      Rewrite_match_redex.match_redex_sequent_hyps:
                             not enough hypotheses when matching hypothesis
                 number 1
# refine axiomVar 2
         Refine error:
     Rewrite_match_redex.match_redex_sequent_hyps: not enough hypotheses
# refine axiomVar (-1)
     Refine error:
         match_redex_sequent_hyps: not enough hypotheses for a negative index
-1

Thanks,

Wojtek