Induction on lists of a specific type does not work

[melanie-taprogge]

When trying to use the induction tactic to proof anything for a list of terms of a specified type rather than an arbitrary type, I receive the error "file:... 𝕃 is not applied to distinct variables."

A very simple example of this:

symbol sample (list : 𝕃 nat) : π (⊤)≔
begin
    induction;
end;

... results in the error, while induction works in cases like...

symbol sample_2 [a] (list : 𝕃 a) : π (⊤)≔
begin
    assume a;
    induction
    {admit}
    {admit}
end;

A lambdapi file with the two examples is attached.
problem.lp.zip

[fblanqui]

fixed in #1142