Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
a,a':Assignment. a' extends a
(
x:Var.
(a x = 3
)
a x = a' x)
Applied Tactic:
UnivCD THENA Auto
Generated subgoals:
1
. a x = a' x
a,a':Assignment. a' extends a 
(x:Var. 
(a x = 3
) a x = a' x)