Verifier seq Compose tree Special Sound

theorem Verifier.seqCompose_treeSpecialSound    (S : ∀ i, ChallengeTreeShape (pSpec i))    (rel : ∀ i, Set (Stmt i × Wit i))    (hWit : Nonempty (Wit (Fin.last m)))    (V : ∀ i, Verifier oSpec (Stmt i.castSucc) (Stmt i.succ) (pSpec i))    (hV : ∀ i, (V i).IsPure)    (h : ∀ i, (V i).treeSpecialSound init impl (S i) (rel i.castSucc) (rel i.succ)) :      (Verifier.seqCompose Stmt V).treeSpecialSound init impl        (ChallengeTreeShape.seqCompose S) (rel 0) (rel (Fin.last m)) := by  induction m with  | zero =>    haveI : Nonempty (Wit 0) := hWit    rw [Verifier.seqCompose_zero]    exact Verifier.id_treeSpecialSound init impl (ChallengeTreeShape.seqCompose S) (rel 0)  | succ m ih =>    rw [Verifier.seqCompose_succ, ChallengeTreeShape.seqCompose_succ]    obtain ⟨f₀, hf₀⟩ := (hV 0).is_pure    have htail := ih (fun i => S i.succ) (fun i => rel i.succ) hWit      (fun i => V i.succ) (fun i => hV i.succ) (fun i => h i.succ)    refine Verifier.append_treeSpecialSound init impl (V 0)      (Verifier.seqCompose (Stmt ∘ Fin.succ) (fun i => V i.succ))      (S 0) (ChallengeTreeShape.seqCompose (fun i => S i.succ)) f₀ hf₀ (h 0) ?_    simpa [Function.comp_def] using htail