simp only [def_iff_]
U V P_U P_V : Formula
l : List VarName
h1_P : Formula
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P))
U V P_U P_V : Formula
l : List VarName
h1_P : Formula
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.imp_ h1_P).and_ (h1_P.imp_ h1_P)))