Working dependent maybeZip

gistfile1.hs

module main

list1 : List Int
list1 = [1, 2, 3]

list2 : List Int
list2 = [4,5,6]

total equalLen : (xs : List a) -> (ys : List b) -> Maybe (length xs = length ys)
equalLen [] [] = Just refl
equalLen (x::xs) (y::ys) = fmap cong $ equalLen xs ys
equalLen _ _ = Nothing

maybeZip : List a -> List b -> Maybe (List (a,b))
maybeZip xs ys = fmap (\p => zip xs ys p) (equalLen xs ys)

main : IO ()
main = print . show $ maybeZip list1 list2