proposition: Lemma PrfEx2: Prf L [A -> B -> C; A; A -> B; A]%fol C.
proof: Proof. change (Prf L ([A -> B -> C; A] ++ [A -> B; A])%fol C); eapply MP. - change [(A -> B -> C)%fol; A] with ([A -> B -> C] ++ [A])%fol; eapply MP. + eapply AXM. + eapply AXM. - change [(A -> B); A]%fol with ([A -> B] ++ [A])%fol; eapply MP. + eapply AXM. + eapply AXM. Qed.
imports: Coq(Arith Lists.List) hydras.Ackermann(fol folProp folProof Languages folLogic folLogic2 folLogic3 subAll Deduction primRec)