rzk-0.8.0: test/typecheck/cases/happy-refl-path.rzk

#lang rzk-1

#define self-path (A : U) (x : A)
  : x =_{A} x
  := refl_{x}

#check self-path : (A : U) -> (x : A) -> x =_{A} x