proposition: Lemma forallE (T : System) (f : Formula) (v : nat) (t : Term): SysPrf T (allH v, f)%fol -> SysPrf T (substF f v t).
proof: Proof. intro H; apply impE with (forallH v f); [| exact H]. - exists (nil (A:=Formula)), (FA1 L f v t); contradiction. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(ListExt folProof folProp Deduction)