Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
F,F':Formula. Dec(F = F')
Applied Tactic:
InstLemma `discrete__Formula` [] THENA Auto THEN UnfoldTopAb (-1)
Generated subgoals:
1
.
F,F':Formula. Dec(F = F')
F,F':Formula. Dec(F = F')F,F':Formula. Dec(F = F')