Level: Lib Thy Top:
Hypotheses:None
Conclusion:
concl,M,N:Formula List. f2:Formula. a:Assignment.
a |
<M @ N, f2::concl> 
a | <M @ (
f2::N), concl>
Applied Tactic: UnivCD THENA Auto
Generated subgoals:1. a | <M @ N, f2::concl> a | <M @ (f2::N), concl>