fact: Fixpoint list_nat_eq (l1 l2: list nat) {struct l1}: bool := match l1, l2 with nil, nil => true | n1::l3, n2::l4 => if Nat.eqb n1 n2 then list_nat_eq l3 l4 else false | _, _ => false end.
imports: List ListAux UList OrderedList