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