diff options
| -rw-r--r-- | src/Util/HList.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/HList.v b/src/Util/HList.v index 120d898d9..1a23f8fd6 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -59,3 +59,7 @@ Proof. rewrite <- IHn; clear IHn. rewrite <- (@Tuple.map_S n _ _ f); destruct ts; reflexivity. } Qed. + +Lemma map_is_mapt' {n A F B} (f : A -> B) {ts : tuple A (S n)} (ls : hlist' F ts) + : Tuple.map f ts = mapt' (fun x _ => f x) ls. +Proof. apply (@map_is_mapt (S n)). Qed. |