proposition: Lemma ded2: SysPrf L (Empty_set _) (A -> A)%fol.
proof: Proof. apply DeductionTheorem. Search SysPrf. apply Axm. Search Add. apply In_add1. Qed.
imports: Coq(Arith Lists.List) hydras.Ackermann(fol folProp folProof Languages folLogic folLogic2 folLogic3 subAll Deduction primRec)