proposition: Lemma derE {n Gamma t} : der Gamma n t -> match n with | 0 => False | S m => exists (ζ: nat -> formula) (s: formula) (k: nat), In s Gamma /\ Forall (der Gamma m) (arguments k (substitute ζ s)) /\ target k (substitute ζ s) = t end.
proof: Proof. case=> *. do 3 eexists. by eauto. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC