| normalize in ⊢ (%→?); #H destruct (H) ]
| #_ % // % %2 // ] ]
| #a #Ha cases (true_or_false (is_sep a)) #Hsep
[ %{2} %
[| % [ %
[ whd in ⊢ (??%?); >(parmove_q0_q2_sep … Hsep) /2/
| normalize in ⊢ (%→?); #H destruct (H) ]
| #_ % // % %2 // ] ]
| #a #Ha cases (true_or_false (is_sep a)) #Hsep
[ %{2} %
[| % [ %
[ whd in ⊢ (??%?); >(parmove_q0_q2_sep … Hsep) /2/