Post steps V

lemma post_stepsV (alice : Alice) (bob : Bob) (vera : Vera) :    (stepsV alice bob n).allow_all >>= postV vera = steps alice bob vera n := by  induction' n with n h  · simp only [Nat.zero_eq, Comp.allow_all, Comp.allow, postV, pure_bind, steps]  · simp only [stepsV, Comp.allow_all_bind, bind_assoc, steps, ← h]    apply congr_arg₂ _ rfl ?_    ext x; induction' x with n y p    · simp only [Comp.allow_all_pure, postV, pure_bind, bind_assoc]    · simp only [stepV, Comp.sample'_bind, pure_bind, Comp.allow_all_bind, Comp.allow_all_allow,        bind_assoc, postV, step]      apply congr_arg₂ _ rfl ?_; ext p; apply congr_arg₂ _ rfl ?_; ext b      induction b      · simp only [ite_false, Comp.allow_all_pure, pure_bind, postV]      · simp only [ite_true]        rw [Comp.allow_all, Comp.allow, bind_assoc]        simp only [Comp.allow, pure_bind, Comp.sample'_bind, postV]