proposition: Theorem zip_eq_nil_l : forall (A B : Set)(lsa : list A)(lsb : list B), zip lsa lsb = nil -> length lsa = length lsb -> lsa = nil.
proof: Proof. induction lsa; intuition; simpl in *. destruct lsb; simpl in *. lia. discriminate. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation