Different types of equality in F*

F* has 3 different types of equality:

val (=)  : #a:Type{hasEq a} -> a -> a -> Tot bool
val (==) : #a:Type -> a -> a -> Tot Type0
val (===): #a:Type -> #b:Type -> a -> b -> Tot Type0

Here is what each of them means:

• = is boolean equality that is automatically generated by F* for many types with decidable equality; such types satisfy the hasEq predicate.
• == is homogeneous propositional equality, and is defined for all F* types the ones without hasEq (this is defined in prims.fst as a squashed inductive)
• === is heterogeneous propositional equality; this more exotic equality is sometimes also called "John Major equality" (this is defined in prims.fst as a squashed inductive)