Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
P,Q:T
.
x,y:T.
L:T List. x = y
(P[x]
Q[y])
(
z
L.P[z]
z
L.Q[z])
Applied Tactic:
Fiat
Generated subgoals:
None
T:
. P,Q:T 
. x,y:T. L:T List. x = y 
(P[x] 
Q[y]) (z
L.P[z] zL.Q[z])