proposition: Lemma existSys (T : System) (f g : Formula) (v : nat): ~ In_freeVarSys L v T -> ~ In v (freeVarF g) -> SysPrf (Ensembles.Add T f) g -> SysPrf (Ensembles.Add T (exH v, f)%fol) g.
proof: Proof. intros H H0 H1; eapply existE. - intros [x H2]; destruct H. exists x. destruct H2 as [H2 H3]; split. + apply H2. + destruct H3 as [x H3| x H3]. * assumption. * induction H3; simpl in H2; absurd (v = v). -- eapply in_remove_neq. apply H2. -- reflexivity. - assumption. - apply Axm; right; constructor. - apply sysWeaken; now apply impI. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(ListExt folProof folProp Deduction)