fact: Fixpoint path_tob (b: T1) (s: seq nat) (a:T1): bool := match s with | [::] => false | [:: i] => (i != 0) && transitionb i a b | i :: s => (i != 0) && path_tob b s (canon a i) end.
imports: mathcomp(all_ssreflect zify) hydras(Canon Paths) gaia_hydras(T1Bridge GCanon) hydras(T1) gaia(ssete9)