fact: Fixpoint pathbdir (swapfirst : bool) l := (match l with | [] => true | [(_, _)] => true | (x, y) :: (((z, t) :: _) as l) => let xy := if swapfirst then x else y in ((xy =? z) && pathbdir false l) || ((xy =? t) && pathbdir true l) end)%bool.
imports: Arith List Permutation