proposition: Lemma peirce : SysPrf L Empty_set Peirce.
proof: Proof. Proof with auto with sets. unfold Peirce; apply impI. eapply orE with (~A)%fol A%fol; [apply noMiddle | | apply impRefl]. apply impI; eapply impE with (A -> B)%fol. - apply Axm ... - apply impI; apply contradiction with A; apply Axm ... Qed.
imports: Coq(Arith Lists.List) hydras.Ackermann(fol folProp folProof Languages folLogic folLogic2 folLogic3 subAll Deduction primRec)