proposition: Lemma impForall (f1 f2 : Formula) (v : nat) (T : System): ~ In_freeVarSys _ v T -> SysPrf T (impH f1 f2) -> SysPrf T (impH (forallH v f1) (forallH v f2)).
proof: Proof. intros H H0; apply (impI L), (forallI L). - intros [x [H1 H2]]; destruct H2 as [x H2| x H2]; [ idtac | induction H2 ]. + apply H; exists x; now split. + apply (in_remove_neq _ _ _ _ _ H1); easy. - apply impE with f1. + apply sysWeaken, H0. + eapply forallSimp. apply Axm; right; constructor. Qed.
imports: Coq(Ensembles Lists.List Peano_dec) hydras.Ackermann(ListExt folProof folLogic folProp)