Of Env swf for policies

theorem ofEnv_swf_for_policies  {Γ : TypeEnv} {ps ps' : Policies}  (hwf : Γ.WellFormed)  (hwt : wellTypedPolicies ps Γ = .ok ps') :  (SymEnv.ofEnv Γ).StronglyWellFormedForPolicies ps':= by  simp only [    SymEnv.StronglyWellFormedForPolicies,    SymEnv.StronglyWellFormedForAll,  ]  constructor  · exact ofEnv_is_swf hwf  · intros tx hmem_tx    have ⟨p', hmem_p', hp'⟩ := List.mem_map.mp hmem_tx    simp only [wellTypedPolicies] at hwt    have ⟨p, hmem_p, hp⟩ := List.mapM_ok_implies_all_from_ok hwt p' hmem_p'    have ⟨_, h⟩ := ofEnv_swf_for_policy hwf hp    simp only [hp'] at h    exact h