Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
(
T,eq,L1,L2,z.L1(
eq)L2)
T:
eq:(T
T
)
L1:T List
L2:T List
True
Applied Tactic:
ProveOpCombTyping `sublist_wf`
Generated subgoals:
None
(
T,eq,L1,L2,z.L1(
eq)L2) 
T:
eq:(T T 
) L1:T List L2:T List 
True