proposition: Lemma existE (T : System) (f g : Formula) (v : nat): ~ In_freeVarSys L v T -> ~ In v (freeVarF g) -> SysPrf T (exH v, f)%fol -> SysPrf T (f -> g)%fol -> SysPrf T g.
proof: Proof. intros H H0 H1 H2. apply nnE. apply impE with (~ (allH v, ~ f))%fol. - apply cp2, impI. apply impE with (allH v, ~ g)%fol. + apply impE with (allH v, ~ g -> ~ f)%fol. * exists (nil (A:=Formula)). exists (FA3 L (~g)%fol (~f)%fol v). contradiction. * apply sysWeaken. apply forallI. -- apply H. -- now apply cp2. + apply impE with (~ g)%fol. * exists (nil (A:=Formula)). exists (FA2 L (~ g)%fol v H0); contradiction. * apply Axm; right; constructor. - apply H1. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(ListExt folProof folProp Deduction)