Beginning of Section Eq
Variable A : SType
Definition. We define
eq to be
λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type
A → A → prop.
End of Section Eq
Notation. We use
= as an infix operator with priority 502 and no associativity corresponding to applying term
eq.
Beginning of Section Ex
Variable A : SType
Definition. We define
ex to be
λQ : A → prop ⇒ ∀P : prop, (∀x : A, Q x → P) → P of type
(A → prop) → prop.
End of Section Ex
Notation. We use
∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex.
Primitive. The name
Eps_i is a term of type
(set → prop) → set.
Primitive. The name
Empty is a term of type
set.
Primitive. The name
ordsucc is a term of type
set → set.
Notation. Natural numbers 0,1,2,... are notation for the terms formed using
Empty as 0 and forming successors with
ordsucc.
Primitive. The name
nat_p is a term of type
set → prop.
Primitive. The name
add_nat is a term of type
set → set → set.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat.
Primitive. The name
TwoRamseyProp is a term of type
set → set → set → prop.
Axiom. (
nat_4) We take the following as an axiom:
Axiom. (
nat_8) We take the following as an axiom:
Axiom. (
add_nat_8_4) We take the following as an axiom:
Proof:
rewrite the current goal using
add_nat_8_4 (from right to left).
∎