proposition: Lemma TreeT1K : pcancel T12Tree Tree2T1.
proof: Proof. elim => // t Ht n t0 Ht0 /=; by rewrite Ht0 Ht. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0) gaia_hydras(T1Bridge)