Theorem relation_fold
Theorem.
relation_fold
(∀t. t ∈ R → ∃x. ∃y. t = (x, y)) → relation R
Proof
relation_fold. ⊢ (∀t. t ∈ R → ∃x. ∃y. t = (x, y)) → relation R,
bij_elimr
relation_equi
.