subst_all and split_intros_goal_wp do not substitute enough
In example verify_this_2018_rouge_et_noir_1, on the last subgoal VC_enum, after split_intros_goal_wp is applied, constant to be substituted remain in subgoal 37 like o o1 etc (as described during gt). Applying subst_all does not work too. subst seems to work in this case.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information