-change with (f tb < f ta) in ⊢ (%→?); @(nat_elim1 (f tb))
-#x lapply (refl ? x) cases x in ⊢ (???%→%);
-[ #Hx
-*
-#x #IH #Hx cases
-
- @IH % #tc change with (f tc < f tb) in ⊢ (%→?);
-
- )(|left @(nat_elim1 (|left ? (nth ? (tape ?) t (niltape ?))|
- +|option_cons sig (current ? (nth dst (tape ?) t (niltape ?)))
- (right ? (nth dst (tape ?) t (niltape ?)))|))
-<(change_vec_same … t dst (niltape ?))
-<(change_vec_same … t src (niltape ?)) in ⊢ (???(???%??));
-lapply (refl ? (nth dst (tape sig) t (niltape ?)))
-cases (nth dst (tape sig) t (niltape ?)) in ⊢ (???%→?);
-[ #Htape_dst % #t1 whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //]
- >Hmid_src #HR cases (HR ?? (refl ??)) -HR
- >nth_change_vec // >Htape_dst #_ * #s0 * normalize in ⊢ (%→?); #H destruct (H)
-| #x0 #xs0 #Htape_dst % #t1 whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //]
- >Hmid_src #HR cases (HR ?? (refl ??)) -HR
- >nth_change_vec // >Htape_dst #_ normalize in ⊢ (%→?);
- * #s0 * #H destruct (H)
-| #x0 #xs0 #Htape_dst % #t1 whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //]
- >Hmid_src #HR cases (HR ?? (refl ??)) -HR
- >nth_change_vec // >Htape_dst #_ normalize in ⊢ (%→?);
- * #s0 * #H destruct (H)
-| #ls #s #rs lapply s -s lapply ls -ls lapply Hmid_src lapply t -t elim rs
- [#t #Hmid_src #ls #s #Hmid_dst % #t1 whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //]
- >Hmid_src >nth_change_vec // >Hmid_dst #HR cases (HR ?? (refl ??)) -HR
- >change_vec_change_vec #Ht1 #_ % #t2 whd in ⊢ (%→?);
- >Ht1 >nth_change_vec_neq [|@sym_not_eq //] >Hmid_src #HR
- cases (HR ?? (refl ??)) -HR #_
- >nth_change_vec // * #s1 * normalize in ⊢ (%→?); #H destruct (H)
- |#r0 #rs0 #IH #t #Hmid_src #ls #s #Hmid_dst % #t1 whd in ⊢ (%→?);
- >nth_change_vec_neq [|@sym_not_eq //] >Hmid_src
- #Htrue cases (Htrue ?? (refl ??)) -Htrue >change_vec_change_vec
- >nth_change_vec // >Hmid_dst whd in match (tape_move_mono ???); #Ht1
- * #s0 * whd in ⊢ (??%?→?); #H destruct (H) #_ >Ht1
- lapply (IH t1 ? (s0::ls) r0 ?)
- [ >Ht1 >nth_change_vec //
- | >Ht1 >nth_change_vec_neq [|@sym_not_eq //] @Hmid_src
- | >Ht1 >nth_change_vec // ]
- ]
-]
-qed. *)