proposition: Lemma impE (T : System) (f g : Formula): SysPrf T (g -> f)%fol -> SysPrf T g -> SysPrf T f.
proof: Proof. intros [x [px Hx]] [x1 [px1 Hx1]]. set (A1 := MP L _ _ _ _ px px1); exists (x ++ x1), A1. intros g0 H; case (in_app_or _ _ _ H); auto. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(ListExt folProof folProp Deduction)