proposition: Lemma eq_unit (a b: unit): a = b.
proof: Proof. by case a; case b. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop bij)