Add exact parent grading without losing extraction copies

import Definitions.Def_mme_recursive_profiled_CW_data

open BigOperators MME MME.ProfiledCW MME.RecursiveYZ MME.CompleteSplit
open scoped Classical
set_option autoImplicit false

theorem mme_exact_step_source_add_parent_grading
    {ell N : ℕ} {P : Predicate N} (E : ExactStep ell N P) :
    ∃ F : ExactStep ell N (fun i x => P i x ∧
      ∀ (r : Fin E.hash.R) (t : Fin (E.hash.n r)),
        (∑ h : Fin 2, ∑ q,
          ((split E.stage.positions E.length x) ⟨r,t,h⟩ q).val) = E.hash.parent r i),
      F.count = E.count ∧ F.stage.repairExponent = E.stage.repairExponent ∧
      F.copies = E.copies ∧ F.output = E.output := by sorry