Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

a:Assignment. q,r:Formula. a |= qr a |= q a |= r

Applied Tactic: UnivCD THENA Auto THEN D 0 THENA Auto THEN Unfolds ``formula_sat formula_falsifiable`` 0 THEN Reduce 0
Generated subgoals:

1. (q under a) (r under a) = 3 (q under a) = 3 (r under a) = 3

2. (q under a) (r under a) = 3 (q under a) = 3 (r under a) = 3