by
  change ∀ script : List (Sum Nat (Sum Nat Nat)),
    script.foldr (fun edit n => match edit with | .inl _ => n | .inr _ => n + 1) 0 +
    2 * script.foldr (fun edit n => match edit with | .inl _ => n + 1 | .inr _ => n) 0 =
    (script.filterMap (fun edit => match edit with | .inl x => some x | .inr (.inl x) => some x | .inr (.inr _) => none)).length +
    (script.filterMap (fun edit => match edit with | .inl x => some x | .inr (.inl _) => none | .inr (.inr x) => some x)).length
  intro script
  induction script with
  | nil => rfl
  | cons edit script ih =>
    cases edit with
    | inl x => simp only [List.foldr_cons, List.filterMap_cons, List.length_cons]; omega
    | inr edit =>
      cases edit with
      | inl x => simp only [List.foldr_cons, List.filterMap_cons, List.length_cons]; omega
      | inr x => simp only [List.foldr_cons, List.filterMap_cons, List.length_cons]; omega