proposition: Lemma silly2_eassumption : 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: Proof. intros P Q HP HQ. destruct HP as [y HP']. eapply HQ. eassumption. Qed.
imports: Coq(Lia) LF(Maps) LF(Imp)