-- Copyright 2020 INP Toulouse.
-- Authors : Mathieu Montin.

-- This version of Irrelevance is provided to you free of charge. It is released under the FSF GPL license, http://www.fsf.org/licenses/gpl.html. 
-- As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users  are provided only 
-- with a limited warranty and the software's author, the holder of the economic rights, and the successive licensors have only limited liability. 
-- In this respect, the user's attention is drawn to the risks associated with loading, using, modifying and/or developing or reproducing the 
-- software by the user in light of its specific status of free software, that may mean that it is complicated to manipulate, and that also there-
-- fore means that it is reserved for developers and experienced professionals having in-depth computer knowledge. Users are therefore encouraged 
-- to load and test the software's suitability as regards their requirements in conditions enabling the security of their systems and/or data to 
-- be ensured and, more generally, to use and operate it in the same conditions as regards security.
-- The fact that you are presently reading this means that you have had knowledge of the FSF GPL version 3 license and that you accept its terms.

open import Data.Nat
open import Relation.Binary.PropositionalEquality

module Irrelevance where

data SList (bound : ) : Set where
  []    : SList bound
  scons : (head : ) 
         .(head  bound)  -- note the dot!
          (tail : SList head) 
          SList bound

postulate
  5≤5₁ : 5  5
  3≤5₁ : 3  5
  0≤3₁ : 0  3

private
  5≤5₂ : 5  5
  5≤5₂ = s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))
  3≤5₂ : 3  5
  3≤5₂ = s≤s (s≤s (s≤s z≤n))
  0≤3₂ : 0  3
  0≤3₂ = z≤n

sl₁ : SList 5
sl₁ = scons 5 5≤5₁ (scons 3 3≤5₁ (scons 0 0≤3₁ []))

sl₂ : SList 5
sl₂ = scons 5 5≤5₂ (scons 3 3≤5₂ (scons 0 0≤3₂ []))

sl₁≡sl₂ : sl₁  sl₂
sl₁≡sl₂ = refl