substitution of prop in fol preserves validity

Stream: maths

[Patrick Thomas]

I was wondering if anyone might see a path forward to prove the forall_ and exists_ cases of thm_13 in the attached. It is a lemma for the last example proof in the file, which is that the uniform simultaneous replacement of the propositions in a formula by formulas preserves validty, if the substitution is defined to do alpha conversion at the same time (the formula_sub_prop_formula function).

pred.lean