proposition: Lemma silly1 : forall (P : nat -> nat -> Prop) (Q : nat -> Prop), (forall x y : nat, P x y) -> (forall x y : nat, P x y -> Q x) -> Q 42.
proof: Proof. intros P Q HP HQ. eapply HQ. apply HP. Abort. Lemma silly2 : forall (P : nat -> nat -> Prop) (Q : nat -> Prop), (exists y, P 42 y) -> (forall x y : nat, P x y -> Q x) -> Q 42. Proof. intros P Q HP HQ. eapply HQ. destruct HP as [y HP']. Fail apply HP'. Abort. Lemma silly2_fixed : forall (P : nat -> nat -> Prop) (Q : nat -> Prop), (exists y, P 42 y) -> (forall x y : nat, P x y -> Q x) -> Q 42. Proof. intros P Q HP HQ. destruct HP as [y HP']. eapply HQ. apply HP'. Qed.
imports: Coq(Lia) LF(Maps) LF(Imp)