simp only [def_and_]
P_r P_s : Formula
r s : VarName
h2 : ¬isBoundIn r true_
h3 : ¬isBoundIn s true_
⊢ IsProof ((eq_ r s).imp_ ((true_.imp_ true_).and_ (true_.imp_ true_)))
P_r P_s : Formula
r s : VarName
h2 : ¬isBoundIn r true_
h3 : ¬isBoundIn s true_
⊢ IsProof ((eq_ r s).imp_ ((true_.imp_ true_).imp_ (true_.imp_ true_).not_).not_)