Thanks for the MR.
We usually use _1
and _2
for the → versions of a ↔
lemma.
So app_nil_1_l
and app_nil_1_r
would be better.
Could we also have app_nil_2 : l1 = [] → l2 = [] → l1 ++ l2 = []
for completeness sake?
added S-waiting-for-author label