Relation.v 290 Bytes
Newer Older
1
(* This file is generated by Why3's Coq-realize driver *)
2 3 4 5 6 7 8 9 10 11
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require set.Set.

(* Why3 assumption *)
Definition rel (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b} :=
  (set.Set.set (a* b)%type).