Proof 01. 1 ⊢ A, hypo. 02. 2 ⊢ ¬A, hypo. 03. 1, 2 ⊢ ⊥, neg_elim 2 1. 04. 1 ⊢ ¬¬A, neg_intro 3. dn_intro. ⊢ A → ¬¬A, subj_intro 4.