[Logiweb] Meta-variables in side conditions

[Frederik Eriksen]

Hi logiweb at diku.dk

Suppose you have a lemma in which a meta-variable 'X' appears in a 
side-condition, but not anywhere else in the lemma. When using the 
lemma, is it necessary to tell the proof checker explicitly how to 
instantiate X? (I know it was necessary last year, but things might have 
changed in the meantime).

Best Regards
Frederik Eriksen.