Lean vs LiquidHaskell for proofs about Haskell programs

Proofs.hs

import Language.Haskell.Liquid.ProofCombinators 


{-@ reflect map1 @-}
map1 :: (Int -> Int) -> [Int] -> [Int]
map1 f [] = []
map1 f (x:xs) = (f x):(map1 f xs)

{-@ reflect length1 @-}
length1 :: [Int] -> Int
length1 [] = 0
length1 (_:xs) = 1 + length1 xs

{-@ p :: f : (Int -> Int) -> xs : [Int]  -> { length1 (map1 f xs) == length1 xs } @-}
p :: (Int -> Int) -> [Int] -> Proof
p f xs = case xs of
    [] ->  length1 (map1 f [])
        === length1 []
        *** QED

    (x:xs) ->  length1 (map1 f (x:xs))
        === length1 ((f x) : (map1 f xs)) 
--        === 1 + length1 (map1 f xs) 
        ? p f xs 
--        === 1 + length1 xs 
        === length1 (x:xs)
        *** QED

Proofs.lean

def map1 (f : Int → Int) : List Int → List Int
| [] => []
| (x::xs) => f x :: map1 f xs

def length1 : List Int → Int
| [] => 0
| (_::xs) => 1 + length1 xs

-- Version using tactics and automation
theorem map_has_same_length (xs: List Int) (f:Int → Int) : 
  length1 (map1 f xs) = length1 xs := by
  induction xs with simp [length1]
  | cons hd tl tl_ih => simp [tl_ih]
  


-- Version similar to the one used in class
theorem map_has_same_length_calc (xs: List Int) (f:Int → Int) : 
  length1 (map1 f xs) = length1 xs := by
  induction xs with
  | nil => calc
    length1 [] = 0 := (by simp)
  | cons hd tl tl_ih => calc 
    length1 (map1 f (hd::tl)) = length1 ((f hd) :: map1 f tl) := (by simp [map1])
                            _ = 1 + length1 (map1 f tl)       := (by simp [length1])
                            _ = 1 + length1 tl                := (by simp [tl_ih])
                            _ = length1 (hd :: tl)            := (by simp [length1])

Right now we do proofs on paper in Functional Programming course. I feel like giving an interactive theorem prover could improve their experience. These are some alternatives that seem reasonable for me.