exact h1_right_right_right_left
case a.h1.h1.h2
P_v : Formula
u v : VarName
h1_right_left : ¬isFreeIn u P_v
h1_right_right_right_left : fastAdmits v u P_v
h1_left : ¬isFreeIn v (fastReplaceFree v u P_v)
h1_right_right_left : fastAdmits u v (fastReplaceFree v u P_v)
h1_right_right_right_right_left : P_v = fastReplaceFree u v (fastReplaceFree v u P_v)
⊢ fastAdmits v u P_v
no goals