Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T,U:. t1,t2:T. u1,u2:U. {t1 = t2} {u1 = u2} {<t1, u1> = <t2, u2>}

Applied Tactic: UnivCD THENA Auto
Generated subgoals:

1. <t1, u1> = <t2, u2>