proposition: Lemma indep_general_premises : forall A `{Inhab A} (P : A -> Prop) (Q : Prop), (Q -> exists x, P x) -> (exists x, Q -> P x).
proof: Proof. Proof using. introv I M. destruct (prop_inv Q). destruct* (M H). exists (arbitrary (A:=A)). auto_false. Qed.
imports: TLC(LibTactics)