proposition: Lemma transitionP i a b : reflect (transition i a b ) (transitionb i a b).
proof: Proof. rewrite /transition /transitionb => //; by apply and3P. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon Paths) gaia_hydras(T1Bridge GCanon) hydras(T1) gaia(ssete9)