Assume H1.
Set F0 to be the term U.
Set F1 to be the term λX Y f : set ⇒ f.
Let X be given.
Assume _.
An exact proof term for the current goal is TrueI.
An exact proof term for the current goal is H1.
Let X be given.
Assume _.
Use reflexivity.
Let X, Y, Z, f and g be given.
Assume _ _ _ _ _.
Use reflexivity.