fact: Fixpoint list_alphabet_ineq (x y:list alphabet) {struct x} : ineq := match x,y with nil, nil => i_eq | nil, cons a u => i_lt | cons a u, nil => i_gt | cons a u, cons b v => match (alphabet_ineq a b) with i_lt => i_lt | i_eq => list_alphabet_ineq u v | i_gt => i_gt end end.