proposition: Lemma T1le_asym: ssrbool.antisymmetric T1le.
proof: Proof. move => x y; by rewrite -T1eq_le =>/eqP. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0) gaia_hydras(T1Bridge)