open import bool
open import bool-relations using (transitive ; total)

module braun-prop (A : Set)
               (_≤A_ : A → A → 𝔹)
               (≤A-trans : transitive _≤A_)
               (≤A-total : total _≤A_) where

open import braun-tree A _≤A_
open import eq
open import nat
open import logic

data _≈ₜ_ : ∀ {n : ℕ} → braun-tree n → braun-tree n → Set where
  ≈ₜ-empty : bt-empty ≈ₜ bt-empty
  ≈ₜ-node : ∀ {n m} {l l' : braun-tree n} { r r' : braun-tree m} { p p' x}
            → l ≈ₜ l'
            → r ≈ₜ r'
            → (bt-node x l r p) ≈ₜ (bt-node x l' r' p')

isProp : ∀ {ℓ} → Set ℓ → Set ℓ
isProp A = (x y : A) → x ≡ y

isSet : ∀ {ℓ} → Set ℓ → Set ℓ
isSet A = (x y : A) → isProp (x ≡ y)

isProp-⊎ : ∀ {X Y : Set} → (X ∧ Y → ⊥) → (isProp X) → (isProp Y) → isProp (X ⊎ Y)
isProp-⊎ ¬X∧Y pX pY (inj₁ x₁) (inj₁ x₂) = cong inj₁ (pX x₁ x₂)
isProp-⊎ ¬X∧Y pX pY (inj₁ x) (inj₂ y) = ⊥-elim (¬X∧Y (x , y))
isProp-⊎ ¬X∧Y pX pY (inj₂ y) (inj₁ x₁) = ⊥-elim (¬X∧Y (x₁ , y))
isProp-⊎ ¬X∧Y pX pY (inj₂ y) (inj₂ y₁) = cong inj₂ (pY y y₁)

ℕ-set : isSet ℕ
ℕ-set n .n refl refl = refl

isProp-braun : ∀ {n m} → isProp (n ≡ m ∨ n ≡ suc m)
isProp-braun {n} {m} = isProp-⊎ (λ {(refl , ())}) (ℕ-set n m) (ℕ-set n (suc m))

≈ₜ→≡ : ∀ {n} {t₁ t₂ : braun-tree n} → t₁ ≈ₜ t₂ → t₁ ≡ t₂
≈ₜ→≡  ≈ₜ-empty = refl
≈ₜ→≡ {_} {bt-node _ _ _ p} {bt-node _ _ _ p'} (≈ₜ-node l≈ₜl' r≈ₜr')
  with ≈ₜ→≡ l≈ₜl' | ≈ₜ→≡ r≈ₜr' | isProp-braun p p'
... | refl | refl | refl = refl