Theorem equi_refl

Theorem. equi_refl
A ↔ A

Reflexivity law of logical equivalence.

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