Level:
Lib
Thy
Top
:
1
Hypotheses:
f :
(1 + 1)
1
Conclusion:
i:
(1 + 1).
j:{(i + 1)..(1 + 1)
}. f i = f j
Applied Tactic:
(OnMCls [0;1] ArithSimp ...a) THEN (InstConcl [
0
;
1
] ...a) THEN Auto'
Generated subgoals:
None
(1 + 1) 
1
i:(1 + 1). j:{(i + 1)..(1 + 1)
}. f i = f j
0
;1] ...a) THEN Auto'