proposition: Lemma MPSys L (G: System L) (A B: Formula L) : SysPrf L G (A -> B)%fol -> SysPrf L G A -> SysPrf L G B.
proof: Proof. destruct 1 as [x [HAB Hx]]. destruct 1 as [y [HA Hy]]. exists (x ++ y). eexists. refine (MP L x y A B _ _). apply HAB. apply HA. intros g Hg; destruct (in_app_or _ _ _ Hg); auto. Qed.
imports: Coq(Arith Lists.List) hydras.Ackermann(fol folProp folProof Languages folLogic folLogic2 folLogic3 subAll Deduction primRec)