apply IsReplOfFormulaInFormula.diff_
case h1.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ P P.not_.not_
case h1.a.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P = P

case h1.a.a.a.a.a.a.a.a
P : Formula
v : VarName
⊢ P.not_.not_ = P.not_.not_