d:Decl, t1,t2:(
d) List, P:(Label
).
t1 @ t2 | P ~ (t1 | P @ t2 | P)
bs ; a.as' [a / (as' @ bs)] (recursive)
is mentioned by
|
Thm* d:Decl, t1,t2:(d) List, P:(Label).
t1 @ t2 | P ~ (t1 | P @ t2 | P) | [trace_projection_append] |
In prior sections: list 1 mb list 1
Try larger context: GenAutomata