SVA: Local variable flow across "implies"

Does a local variable flow across the “implies” operator?
Consider the two properties below.

property prop1;
logic [7:0] curr_val;
(en_d, curr_val = inval1_d) |-> ((curr_val + 4’d4) == out1);
endproperty

property prop2;
logic [7:0] curr_val;
(en_d, curr_val = inval1_d) implies ((curr_val + 4’d4) == out1);
endproperty

Are these equivalent in terms of local variable flow?
Should the second one result in an error?

I’ve seen some online discussions of something like this from the time of the LRM development.
https://www.eda-twiki.org/sv-ac/hm/9413.html

How was this discussion resolved?
Thanks

The proposal got dropped. 03195: Local Variables Flow Out Issue in and/or/intersect/implies - Accellera Mantis

It’s not an error, but each thread of an assertion gets its own copy of the local variable. Using implies creates threads for both the antecedent and consequent.