try first
| apply verum!;
| apply imply₁!;
| apply imply₂!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply dne!;
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! ~~p✝ ⟶ p✝
no goals