p-free formulas should be interpolants of themselves

[hferee]

Any p-free formula (actually sequent) satisfies the axioms of its uniform interpolants (actually E and A) w.r.t. p.

[hferee]

After giving it some thought, doing this somehow efficiently would require to:

• [ ] embed the type of formulas within a type fomulas (recursively) annotated with their number of occurrences of the variable p to eliminate
• [ ] also annotate the environments with their total number of occurrences of p
• [ ] When computing E/A, first check the number of occurrences of p in the arguments (constant time access). If it's 0, then build the formula from the arguments directly (Δ or Δ -> φ).