module _ (t : Test) where
  open Test t
  testFn : (a ≡ b)
  testFn  = {!!}


test2 : (c d : Nat) → (c ≡ d)
test2 c d = testFn (record {a = c; b = d })