Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

(Alph,L,M,z.L = M) Alph: L:L(Alph) M:L(Alph) True '

Applied Tactic: ProveOpCombTyping `lang_eq_wf`
Generated subgoals:

None