Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

S:Sequent. |= S

Applied Tactic: UnivCD THENA Auto THEN Unfold `sequent_valid` 0
Generated subgoals:

1. (a:Full(S). a |= S)