Level: Lib Thy Top:
Hypotheses:None
Conclusion:
a:Assignment. f:Formula.
h((f eval under a) ) = 3
(
f':Formula. (f eval under a) = (inr f' ))
Applied Tactic: RepeatFor 2 (D 0 THENA Auto)
Generated subgoals:1. h((f eval under a) ) = 3 (f':Formula. (f eval under a) = (inr f' ))