fact: Fixpoint test_list {A: Type} (f : A -> A -> bool) l1 l2 := match l1, l2 with | nil, nil => true | a :: l3, b :: l4 => if f a b then test_list f l3 l4 else false | _, _ => false end.
imports: Ascii String List EqNat NArith