proposition: Lemma T12Tree_inj: injective T12Tree.
proof: Proof. move => t1 t2 Heq. have H: Some t1 = Some t2 by rewrite -!TreeT1K Heq. by injection H. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0) gaia_hydras(T1Bridge)