Let A and B be given.

Assume H1: atleastp A B.

Assume H2: atleastp B A.

Apply H1 to the current goal.

Let f be given.

Assume Hf: inj A B f.

Apply H2 to the current goal.

Let g be given.

Assume Hg: inj B A g.

An exact proof term for the current goal is SchroederBernstein A B f g Hf Hg.

∎