0 | 1 | module Theory.Tuple 2 | 3 | ||| A tuple consists of its first and second element 4 | total 5 | export 6 | tuple_destruct : (t : (a, b)) -> t = (fst t, snd t) 7 | tuple_destruct (x, y) = Refl 8 |