Simplifier should split a label of conjuncts

[ordinarymath]

Given a assumption of foo :- (A /\ B) a goal of A /\ B fs[L"foo"] should be simplified see zulip #❄️ HOL4 > Label of conjuncts should be split.