Commit 66caaa2d authored by Nicola Botta's avatar Nicola Botta
Browse files

Cleanup.

parent 32afa394
module Pair.Properties
> module Pair.Properties
> %default total
> %access public export
> %auto_implicits off
> pairLemma : {A, B : Type} -> (ab : (A, B)) -> ab = (fst ab, snd ab)
> pairLemma (a, b) = Refl
> pairEqElimFst : {A, B : Type} -> {a, a' : A} -> {b, b' : B} -> (a, b) = (a', b') -> a = a'
> pairEqElimFst Refl = Refl
> pairEqElimSnd : {A, B : Type} -> {a, a' : A} -> {b, b' : B} -> (a, b) = (a', b') -> b = b'
> pairEqElimSnd Refl = Refl
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment