For instance, the proof state after the intros. in lookup_total_app_l now looks like
A : Type __Inhabited : Inhabited A l1, l2 : list A i : nat __H : i < length l1 ============================ (l1 ++ l2) !!! i = l1 !!! i
I like it. :) I think we can just always enable this and not have anything extra on CI; we will hopefully notice when proof scripts contain such an identifier starting with __.
