Equality, roughly speaking
In Software Foundations, equality is defined in this way: Even Coq's equality relation is not built in. It has (roughly) the following inductive definition. Inductive eq0 {X:Type} : X -> X -> Prop := refl_equal0 : forall x, eq0 x x. Why the roughly? Well, as it turns out, Coq defines equality a little differently […]