1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Inductive baz :=
K : (let foo2 := Type@{_} in
let foo3 := Type@{_} in
let set_le_foo3 := (fun y : Set => (fun x : foo3 => x) y) in
let foo3_le_foo2 := (fun y : foo3 => (fun x : foo2 => x) y) in
let set_eq_foo2 := (fun y : foo2 => (fun x : Set => x) y) in
nat) -> baz.
(* a bit more transitive constraints *)
Inductive baz' :=
K' : (let foo2 := Type@{_} in
let foo3 := Type@{_} in
let foo4 := Type@{_} in
let set_le_foo3 := (fun y : Set => (fun x : foo3 => x) y) in
let foo3_le_foo2 := (fun y : foo3 => (fun x : foo2 => x) y) in
let foo2_le_foo4 := (fun y : foo2 => (fun x : foo4 => x) y) in
let set_eq_foo4 := (fun y : foo4 => (fun x : Set => x) y) in
nat) -> baz'.
|
