intro _
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ ¬v = u → ¬isFreeIn v P_u
case a.a.h1.h2
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
a✝ : ¬v = u
⊢ ¬isFreeIn v P_u