update cong₂ to ap₂
Add Σ A (_≡_ x) is contractable
Add Any predicate for binary tree