Right Proj tree is Structured

theorem RightProj.tree_isStructured :    {r : Fin (n + 1)} → (R : RightProj S₁.arity S₂.arity r) →    R.src.IsStructured (S₁.append S₂) → R.tree.IsStructured S₂  | _, .leaf, _ => trivial  | _, .msg i h m₂ child, hR => by      have hround : (Fin.natAdd m i).succ = rightRound i.succ := by        apply Fin.ext        simp only [Fin.val_succ, Fin.val_natAdd, rightRound]        omega      simp only [RightProj.src, ChallengeTree.IsStructured] at hR      apply RightProj.tree_isStructured child      convert hR using 1      · exact hround.symm      · rfl  | _, .chal i h chals children, hR => by      have hApp : (pSpec₁ ++ₚ pSpec₂).dir (Fin.natAdd m i) = .V_to_P := by        simpa [ProtocolSpec.append, Fin.vappend_eq_append, Fin.append_right] using h      have hIdx : (⟨Fin.natAdd m i, hApp⟩ : (pSpec₁ ++ₚ pSpec₂).ChallengeIdx)          = ChallengeIdx.inr ⟨i, h⟩ := by ext; rfl      have hAr : appendArity S₁.arity S₂.arity ⟨Fin.natAdd m i, hApp⟩ = S₂.arity ⟨i, h⟩ := by        rw [hIdx]; simpa [appendArity] using          congrArg (Sum.elim S₁.arity S₂.arity)            (ChallengeIdx.sumEquiv_symm_inr (pSpec₁ := pSpec₁) ⟨i, h⟩)      have hR' := hR      simp only [RightProj.src, ChallengeTree.IsStructured] at hR'      refine ⟨?_, fun j => RightProj.tree_isStructured (children j) (hR'.2 (Fin.cast hAr.symm j))⟩      -- `hsymm` is quantified over the dir proof so `simp` rewrites the `match` scrutinee      -- regardless      -- of which (proof-irrelevant) proof term `RightProj.src` inlined.      have hsymm : ∀ (P : (pSpec₁ ++ₚ pSpec₂).dir (Fin.natAdd m i) = .V_to_P),          ChallengeIdx.sumEquiv.symm (⟨Fin.natAdd m i, P⟩ : (pSpec₁ ++ₚ pSpec₂).ChallengeIdx)            = Sum.inr ⟨i, h⟩ := fun P => by        rw [show (⟨Fin.natAdd m i, P⟩ : (pSpec₁ ++ₚ pSpec₂).ChallengeIdx) = ChallengeIdx.inr ⟨i, h⟩          from by ext; rfl, ChallengeIdx.sumEquiv_symm_inr]      have hR1 := hR'.1      simp only [ChallengeTreeShape.append] at hR1      split at hR1      · rename_i i₁ heqs; exact absurd (heqs.symm.trans (hsymm _)) (by simp)      · rename_i i₂ heqs        obtain rfl : i₂ = ⟨i, h⟩ := Sum.inr.inj (heqs.symm.trans (hsymm _))        convert hR1 using 2        simp [cast_cast]