fact: Fixpoint arguments (k: nat) (t: formula) := match k with | 0 => [] | S k => match t with | var _ => [] | arr s t => s :: (arguments k t) end end.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC