Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
f1,f2:{T=
}. f1 = f2
Applied Tactic:
UnivCD THENA Auto
Generated subgoals:
1
. f1 = f2
T:
. f1,f2:{T=
}. f1 = f2