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 Rewrite (HigherC valuation_unrollC) 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