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