Rename iffT, add some lemmas about tuple and hlist

Some lemmas admitted

1 files changed, 20 insertions, 0 deletions

diff --git a/src/Util/HList.v b/src/Util/HList.v
index 1a23f8fd6..0ebb4cdce 100644
--- a/src/Util/HList.v
+++ b/src/Util/HList.v
@@ -63,3 +63,23 @@ 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.
+
+
+Lemma hlist'_impl {n A F G} (xs:tuple' A n)
+  : (hlist' (fun x => F x -> G x) xs) -> (hlist' F xs -> hlist' G xs).
+Proof.
+  induction n; simpl in *; intuition.
+Defined.
+
+Lemma hlist_impl {n A F G} (xs:tuple A n)
+  : (hlist (fun x => F x -> G x) xs) -> (hlist F xs -> hlist G xs).
+Proof.
+  destruct n; [ constructor | apply hlist'_impl ].
+Defined.
+
+Module Tuple.
+  Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n)
+  : hlist (fun x => f x = x) xs -> Tuple.map f xs = xs.
+  Proof.
+  Admitted.
+End Tuple.