Post

hey did you know you're kinda cool proven, in lean theorem you_are_cool {You Cool : Prop} (beingYouIsCool : You → Cool) (justBeYou : You) : Cool := beingYouIsCool justBeYou