proposition: Lemma canon_SSn_zero (i : nat) (a : T1) (n : nat): T1nf a -> canon (cons a n.+1 zero) i = cons a n (canon (phi0 a) i).
proof: Proof. rewrite -(h2g_g2hK a) /canon g2h_cons g2h_h2gK => Hnf; rewrite -h2g_cons h2g_g2hK canon_SSn_zero. congr h2g. move: Hnf; by rewrite h2g_g2hK hnf_g2h. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)