gistfile1.txt

  data _≤2_ : ℕ → ℕ → Set where
    n≤2n :  {m : ℕ} → m ≤2 m
    n≤2s :  {m n : ℕ} → m ≤2 n → m ≤2 suc (n) 

  from-to : {n m : ℕ} {x : n ≤2 m} -> from  (to x) ≡ x
  from-to {.m} {m} {n≤2n} = {!refl!}
  from-to {n} {suc m} {n≤2s y} = cong ({!n≤2s!}) (from-to {n} {m} {y})

>> 
?0 : from (to n≤2n) ≡ n≤2n
?1 : n ≤2 m → n ≤2 suc m

data ≤2 : ℕ → ℕ → Set where
n≤2n : {m : ℕ} → m ≤2 m
n≤2s : {m n : ℕ} → m ≤2 n → m ≤2 suc (n)

from-to : {n m : ℕ} {x : n ≤2 m} -> from (to x) ≡ x
from-to {.m} {m} {n≤2n} = {!refl!}
from-to {n} {suc m} {n≤2s y} = cong ({!n≤2s!}) (from-to {n} {m} {y})

?0 : from (to n≤2n) ≡ n≤2n
?1 : n ≤2 m → n ≤2 suc m

module ConstraintExample where

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

-- An explicit version of refl:

reflx : (n : ℕ) → n ≡ n
reflx n = refl

-- An example of a situation where filling in an expression
-- of the correct type is not sufficient:

example : 2 ≡ 2
example = reflx {!3!}