Can we derive
$${p \hspace{0.1cm} \& \hspace{0.1cm} q, \hspace{0.2cm} p \hspace{0.01cm} \rightarrow \hspace{0.01cm} \neg \thinspace q \hspace{0.2cm} \vdash \hspace{0.2cm}\bot}$$
using $\textit{only}$ elimination rules, structural rules and cut, in an intuitionistic natural deduction in sequent-style calculus (in which the rules are expressed with sequents but there are intro- and elim-rules that act only on consequents)? The relevant elimination rules are:
$$\frac{\Gamma \Rightarrow A \rightarrow B \qquad \Delta \Rightarrow A}{\Gamma, \Delta \Rightarrow B}\hspace{0.1cm} \rightarrow Elim \hspace{0.1cm}$$ $$\frac{\Gamma \Rightarrow A \land B}{\Gamma \Rightarrow A}\hspace{0.1cm} \& Elim_1 \hspace{0.1cm}$$ $$\frac{\Gamma \Rightarrow A \land B}{\Gamma \Rightarrow B}\hspace{0.1cm} \& Elim_2 \hspace{0.1cm}$$ $$\frac{\Gamma \Rightarrow \bot}{\Gamma \Rightarrow A}\hspace{0.1cm} \bot Elim \hspace{0.1cm}$$
This is claimed possible (but not proven) in
- Grigori Mints and Shane Steinert-Threlkeld ADC method of proof search for intuitionistic propositional natural deduction (2016): page 396.
where a version of the natural deduction in sequent-style calculus is presented.
Edit: I have managed to get to $$\frac{\hspace{0.2cm} p \hspace{0.01cm} \rightarrow \hspace{0.01cm} (q \rightarrow \bot) \Rightarrow (p \land q) \rightarrow \bot \qquad p \land q \hspace{0.3cm} \Rightarrow \hspace{0.3cm} p \land q}{p \hspace{0.1cm} \& \hspace{0.1cm} q, \hspace{0.2cm} p \hspace{0.01cm} \rightarrow \hspace{0.01cm} (q \rightarrow \bot) \hspace{0.2cm} \Rightarrow \hspace{0.2cm}\bot}_{\rightarrow \hspace{0.2cm} Elim}$$ But can't prove $\hspace{0.2cm} p \hspace{0.01cm} \rightarrow \hspace{0.01cm} (q \rightarrow \bot) \Rightarrow (p \land q) \rightarrow \bot$