Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

F:Formula. a:Assignment. a |= F a | F


Applied Tactic: UnivCD THENA Auto THEN D 0
Generated subgoals:

1. a |= F a | F

2. a |= F a | F