Thank you SO much, @MargaretJLake (and Margaret’s Granny!)…embroidered lab coat might just be the best win so far….not to mention the amazing job @MargaretJLake did on her first surgeries today!! Super proud and grateful!!🎉🤓🥰❤️

OK, with that in mind, let's revisit the type of the function we want to write: forall (l1 l2 : list T), length l1 = m -> length l2 = n -> length (append l1 l2) = m n What does it do? Well, it will take in two lists as arguments. So let's modus ponens that shit.