Slides of a (very) informal lecture of mine on the Curry-Howard correspondence
1 inductive eq (x y : t) : Prop 2 | rfl : eq x x 3 4 infix = := eq