Incorrect handling of scoping

[MirceaS]

The following simple example illustrates how this Metamath implementation fails to respect the scoping of $e statements.

$( The type of propositions $)
$c prop $.
$c |- true false $.
$v P $.

$( P, true and false are propositions $)
P-prop     $f prop P $.
true-prop  $a prop true $.
false-prop $a prop false $.

$( ex falso quodlibet $)
${
    hyp $e |- false $.
    p   $a |- P $.
$}

$( Proof of false via reference to out-of-scope hypothesis $)
proof-of-false $p |- false $= hyp $.