blob: b3914a1cc47ecb766af99240fcf4744c27e75bb2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Axioms:
foo : nat
Axioms:
foo : nat
Fetching opaque terms in /home/pm/Desktop/sources/coq/theories/Arith/Plus.vo
Fetching opaque terms in /home/pm/Desktop/sources/coq/theories/Init/Peano.vo
Axioms:
extensionality : forall (P Q : Type) (f g : P -> Q),
(forall x : P, f x = g x) -> f = g
Axioms:
extensionality : forall (P Q : Type) (f g : P -> Q),
(forall x : P, f x = g x) -> f = g
Axioms:
extensionality : forall (P Q : Type) (f g : P -> Q),
(forall x : P, f x = g x) -> f = g
Axioms:
extensionality : forall (P Q : Type) (f g : P -> Q),
(forall x : P, f x = g x) -> f = g
Closed under the global context
Closed under the global context
|
