proposition: Lemma ded3 : exists pf : Prf L (nil) (A -> A)%fol , True.
proof: Proof. apply ded1. apply ded2. Qed.
imports: Coq(Arith Lists.List) hydras.Ackermann(fol folProp folProof Languages folLogic folLogic2 folLogic3 subAll Deduction primRec)