Theorem Proving for All Equational Reasoning in Liquid Haskell Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, and Graham Hutton [PDF] 1.Introduction 2.Reasoning about Programs 2.1. Lightweight Reasoning 2.2. Induction on Lists 2.3. Proof Automation 3.Totality and Termination 3.1. Totality Checking 3.2. Termination Checking 3.3. Uncaught termination 4.Function Optimization 4.1. Example: