[ #Hcursrc %{2} %
[| % [ %
[ whd in ⊢ (??%?); >parmove_q0_q2_null_src /2/
- <(nth_vec_map ?? (current …) src ? int (niltape ?)) //
| 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/
- <(nth_vec_map ?? (current …) src ? int (niltape ?)) //
| normalize in ⊢ (%→?); #H destruct (H) ]
| #_ % // % % %{a} % // ] ]
| lapply (refl ? (current ? (nth dst ? int (niltape ?))))
[ #Hcurdst %{2} %
[| % [ %
[ whd in ⊢ (??%?); >(parmove_q0_q2_null_dst … Hsep) /2/
- [ <(nth_vec_map ?? (current …) dst ? int (niltape ?)) //
- | <(nth_vec_map ?? (current …) src ? int (niltape ?)) // ]
| normalize in ⊢ (%→?); #H destruct (H) ]
| #_ % // %2 // ] ]
| #b #Hb %{2} %
[| % [ %
[whd in ⊢ (??%?); >(parmove_q0_q1 … Hneq Hsrc Hdst ? b ?? Hsep) //
- [ <(nth_vec_map ?? (current …) dst ? int (niltape ?)) //
- | <(nth_vec_map ?? (current …) src ? int (niltape ?)) // ]
| #_ %{a} %{b} % // % // % // ]
| * #H @False_ind @H % ]
]]]]