Theorem equi_refl
Theorem.
equi_refl
A ↔ A
Proof
01. 1 ⊢ A,
hypo
. 02. ⊢ A → A,
subj_intro
1. equi_refl. ⊢ A ↔ A,
bij_intro
2 2.