blob: f4eaa9d53f84577338ff07056e57c2b7972e94ed (
plain)
1
2
3
4
5
6
7
8
9
10
|
Require Import Coq.Classes.RelationClasses.
Notation iffT A B := (((A -> B) * (B -> A)))%type.
Notation iffTp := (fun A B => inhabited (iffT A B)).
Global Instance iffTp_Reflexive : Reflexive iffTp | 1.
Proof. repeat constructor; intro; assumption. Defined.
Global Instance iffTp_Symmetric : Symmetric iffTp | 1.
Proof. repeat (intros [?] || intro); constructor; tauto. Defined.
Global Instance iffTp_Transitive : Transitive iffTp | 1.
Proof. repeat (intros [?] || intro); constructor; tauto. Defined.
|
