Conjunction, disjunction and 'xorjunction' implemented on bitvectors. Lots of supporting datatypes. Vectors.ma includes some diabolical dependent type hackery due to Wilmer.