------------------------------------------------------------------------
-- Some cancellation lemmas
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Atom

module Cancellation (atoms : χ-atoms) where

open import Equality.Propositional
open import Prelude hiding (const)

open import Chi    atoms
open import Values atoms

cancel-const :
   {c₁ c₂ es₁ es₂} 
  Exp.const c₁ es₁  const c₂ es₂ 
  c₁  c₂ × es₁  es₂
cancel-const refl = refl , refl

cancel-lambda :
   {x₁ x₂ e₁ e₂} 
  Exp.lambda x₁ e₁  lambda x₂ e₂ 
  x₁  x₂ × e₁  e₂
cancel-lambda refl = refl , refl

cancel-rec :
   {x₁ x₂ e₁ e₂} 
  Exp.rec x₁ e₁  rec x₂ e₂ 
  x₁  x₂ × e₁  e₂
cancel-rec refl = refl , refl

cancel-apply :
   {e₁₁ e₁₂ e₂₁ e₂₂} 
  Exp.apply e₁₁ e₂₁  apply e₁₂ e₂₂ 
  e₁₁  e₁₂ × e₂₁  e₂₂
cancel-apply refl = refl , refl

cancel-case :
   {e₁ e₂ bs₁ bs₂} 
  Exp.case e₁ bs₁  case e₂ bs₂ 
  e₁  e₂ × bs₁  bs₂
cancel-case refl = refl , refl

cancel-var :
   {x₁ x₂} 
  Exp.var x₁  var x₂  x₁  x₂
cancel-var refl = refl

cancel-branch :
   {c₁ c₂ xs₁ xs₂ e₁ e₂} 
  Br.branch c₁ xs₁ e₁  branch c₂ xs₂ e₂ 
  c₁  c₂ × xs₁  xs₂ × e₁  e₂
cancel-branch refl = refl , refl , refl