From 853821e4374050d5a770ee623b24a7bf15e288ae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 8 Nov 2016 11:22:11 -0500 Subject: Rename iffT, add some lemmas about tuple and hlist Some lemmas admitted --- src/Util/IffT.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'src/Util/IffT.v') diff --git a/src/Util/IffT.v b/src/Util/IffT.v index fd132fbfa..f4eaa9d53 100644 --- a/src/Util/IffT.v +++ b/src/Util/IffT.v @@ -1,9 +1,10 @@ Require Import Coq.Classes.RelationClasses. -Notation iffT := (fun A B => inhabited ((A -> B) * (B -> A)))%type. +Notation iffT A B := (((A -> B) * (B -> A)))%type. +Notation iffTp := (fun A B => inhabited (iffT A B)). -Global Instance iffT_Reflexive : Reflexive iffT | 1. +Global Instance iffTp_Reflexive : Reflexive iffTp | 1. Proof. repeat constructor; intro; assumption. Defined. -Global Instance iffT_Symmetric : Symmetric iffT | 1. +Global Instance iffTp_Symmetric : Symmetric iffTp | 1. Proof. repeat (intros [?] || intro); constructor; tauto. Defined. -Global Instance iffT_Transitive : Transitive iffT | 1. +Global Instance iffTp_Transitive : Transitive iffTp | 1. Proof. repeat (intros [?] || intro); constructor; tauto. Defined. -- cgit v1.2.3