From bd28f5b205d54aa014587cbf03a322101fb0b021 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 6 Nov 2016 17:10:45 -0500 Subject: Add more admitted tuple lemmas --- src/Util/Tuple.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/Util/Tuple.v') diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 455c28f00..aca78cd5a 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -172,6 +172,11 @@ Lemma map_id {n A} (xs:tuple A n) Proof. Admitted. +Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n) + : (forall x, f x = x) -> map f xs = xs. +Proof. +Admitted. + Section monad. Context (M : Type -> Type) (bind : forall X Y, M X -> (X -> M Y) -> M Y) (ret : forall X, X -> M X). Fixpoint lift_monad' {n A} {struct n} -- cgit v1.2.3