Append tree Special Sound

theorem append_treeSpecialSound    (V₁ : Verifier oSpec Stmt₁ Stmt₂ pSpec₁)    (V₂ : Verifier oSpec Stmt₂ Stmt₃ pSpec₂)    (S₁ : ChallengeTreeShape pSpec₁) (S₂ : ChallengeTreeShape pSpec₂)    (verify₁ : Stmt₁ → pSpec₁.FullTranscript → Stmt₂)    (hV₁ : ∀ stmt tr, V₁.verify stmt tr = pure (verify₁ stmt tr))    (h₁ : V₁.treeSpecialSound init impl S₁ rel₁ rel₂)    (h₂ : V₂.treeSpecialSound init impl S₂ rel₂ rel₃) :      (V₁.append V₂).treeSpecialSound init impl        (S₁.append S₂) rel₁ rel₃ := by  rcases h₁ with ⟨E₁, hE₁⟩  rcases h₂ with ⟨E₂, hE₂⟩  refine ⟨fun stmt tree => E₁ stmt tree.appendSplit.fst, ?_⟩  intro stmt tree hStructured hAccept  apply hE₁ stmt tree.appendSplit.fst  · exact ChallengeTree.appendSplit_fst_isStructured tree hStructured  · intro tr₁ htr₁    obtain ⟨path, rfl⟩ :=      ChallengeTree.LeafPath.exists_of_mem_fullTranscripts (T := tree.appendSplit.fst) htr₁    have hSuffixStructured :        (tree.appendSplit.sndAt path).IsStructured S₂ :=      ChallengeTree.appendSplit_sndAt_isStructured tree hStructured path    have hSuffixAccept :        (tree.appendSplit.sndAt path).IsAccepting init impl V₂          (verify₁ stmt path.fullTranscript) rel₃.language := by      intro tr₂ htr₂      have hmem :          path.fullTranscript ++ₜ tr₂ ∈ tree.fullTranscripts :=        ChallengeTree.appendSplit_fullTranscripts_append_of_mem tree path htr₂      have hfull := hAccept (path.fullTranscript ++ₜ tr₂) hmem      simpa [append_run_pure_left V₁ V₂ verify₁ hV₁          stmt path.fullTranscript tr₂] using hfull    have hRel₂ :        (verify₁ stmt path.fullTranscript,          E₂ (verify₁ stmt path.fullTranscript) (tree.appendSplit.sndAt path)) ∈ rel₂ :=      hE₂ (verify₁ stmt path.fullTranscript) (tree.appendSplit.sndAt path)        hSuffixStructured hSuffixAccept    have hLang₂ : verify₁ stmt path.fullTranscript ∈ rel₂.language :=      (Set.mem_language_iff rel₂ (verify₁ stmt path.fullTranscript)).2        ⟨E₂ (verify₁ stmt path.fullTranscript) (tree.appendSplit.sndAt path), hRel₂⟩    exact pure_accepting_of_mem init impl V₁ stmt path.fullTranscript rel₂.language      (verify₁ stmt path.fullTranscript) (hV₁ stmt path.fullTranscript) hLang₂