Commit 2020-05-20 19:37 a540d79b

chore(archive/sensitivity): Clean up function coercion in sensitivity proof (depends on #2756) (#2758) This formalizes the proof of an old conjecture: is_awesome Gabriel. I also took the opportunity to remove type class struggling, which I think is related to the proof of is_awesome Floris. I think @jcommelin should also update this sensitivity file to use his sum notations if applicable.