fact: Fixpoint same_first (l1 l2:list(nat*nat)) {struct l1} : bool := match l1, l2 with nil, nil => true | ((a, _)::l'1), ((b, _)::l'2) => match Nat.compare a b with | Eq => same_first l'1 l'2 | _ => false end | _, _ => false end.
imports: List Arith