proposition: Lemma ded1: forall (A: Formula L), (SysPrf L (Empty_set _) A) -> exists pf : Prf L (nil) A, True.
proof: Proof. intros. inversion H. destruct H0. destruct x. exists x0. auto. specialize (H0 f). specialize (H0 (in_eq f x)). destruct H0. Qed.
imports: Coq(Arith Lists.List) hydras.Ackermann(fol folProp folProof Languages folLogic folLogic2 folLogic3 subAll Deduction primRec)