Let X, Y, Z, f and g be given.
Assume Hf.
Assume Hg.
Apply Hf to the current goal.
Assume Hf1 Hf2.
Apply Hg to the current goal.
Assume Hg1 Hg2.
Apply injI to the current goal.
Let u be given.
Assume Hu: u ∈ X.
An exact proof term for the current goal is (Hg1 (f u) (Hf1 u Hu)).
Let u be given.
Assume Hu: u ∈ X.
Let v be given.
Assume Hv: v ∈ X.
Assume H1: g (f u) = g (f v).
We will prove u = v.
Apply Hf2 u Hu v Hv to the current goal.
We will prove f u = f v.
Apply Hg2 (f u) (Hf1 u Hu) (f v) (Hf1 v Hv) to the current goal.
We will prove g (f u) = g (f v).
An exact proof term for the current goal is H1.
∎