{-# OPTIONS --exact-split #-}

open import Agda.Builtin.Nat using (Nat; zero; suc)
open import Agda.Builtin.Equality

data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

_≢_ : {A : Set} → A → A → Set
x ≢ y = x ≡ y → ⊥

data Expr : Set where
  :0   : Expr
  gen  : Nat → Expr
  _+_  : Expr → Expr → Expr

data f-View : Expr → Expr → Set where
  instance
    f0y : {y : Expr}   → f-View :0 y
    fx0 : {x : Expr}   → f-View x  :0
    fxy : {x y : Expr} → f-View x  y

f-view : (x y : Expr) → f-View x y
f-view :0        y         = f0y
f-view (gen x)   :0        = fx0
f-view (gen x)   (gen y)   = fxy
f-view (gen x)   (y₁ + y₂) = fxy
f-view (x₁ + x₂) :0        = fx0
f-view (x₁ + x₂) (gen y)   = fxy
f-view (x₁ + x₂) (y₁ + y₂) = fxy

f : (x y : Expr) → Expr
f x y with f-view x y
f .:0 y   | f0y = y
f x   .:0 | fx0 = x
f x   y   | fxy = x + y

lemma :  ∀ {x y} → x ≢ :0 → y ≢ :0 → f x y ≡ x + y
lemma {x}   {y}   p q with f-view x y
lemma {.:0} {y}   p q | f0y = ⊥-elim (p refl)
lemma {x}   {.:0} p q | fx0 = ⊥-elim (q refl)
lemma {x}   {y  } p q | fxy = refl