+(*BEGIN*)
+apply rule (⇒_i [h1] (∀x.P x ⇒ Q c));
+apply rule (∀_i {l} (P l ⇒ Q c));
+apply rule (⇒_i [h2] (Q c));
+apply rule (⇒_e ((∃x.P x) ⇒ Q c) (∃x.P x));
+ [ apply rule (discharge [h1]);
+ | apply rule (∃_i {l} (P l));
+ apply rule (discharge [h2]);
+ ]
+(*END*)