Using a mélange of mathematical syntaxes, we mechanize some exercises from Tao's excellent book

## Ouverture

Let us informally define sets and set membership

The axiom of substition uses the definition of equality:

The axiom of substition is preserved for all sets only defined in terms of

Verify that set equality is reflexive, symmetric, and transitive.

Goal:

Hypothesis:

Proof.

Qed.

Prove that the following sets are distinct:

Hypothesis:

Lemma:

Proof.

Qed.

Show that, for any set

Hypothesis:

Proof.

Qed.

Show that, for any three sets

Hypothesis:

Proof.

Qed.

Show that, for any two sets

Hypothesis:

Proof.

Qed.

(3.3.4) Show that injective corresponds to left-cancelable, and dually, surjective corresponds to right-cancelable, in function composition.

For this proof, we use natural deductions, as introduced in Dowek's Proofs in Theories Ch. 1.

where