proposition: Lemma forallI (T : System) (f : Formula) (v : nat): ~ In_freeVarSys L v T -> SysPrf T f -> SysPrf T (allH v, f)%fol.
proof: Proof. intros H [x [x0 H0]]; exists x. assert (~ In v (freeVarListFormula L x)). { intro H1; apply H. destruct (In_freeVarListFormulaE _ _ _ H1) as [x1 H2]. exists x1; split. - tauto. - apply H0; tauto. } exists (GEN L _ _ _ H1 x0); apply H0. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(ListExt folProof folProp Deduction)